| #
f2ad1c56 |
|
01-Sep-2017 |
wenzelm <none@none> |
more robust: provide docking framework via base plugin;
--HG--
rename : src/Tools/jEdit/src/dockable.scala => src/Tools/jEdit/src-base/dockable.scala
rename : src/Tools/jEdit/src/pide_docking_framework.scala => src/Tools/jEdit/src-base/pide_docking_framework.scala
|
| #
3891c3e0 |
|
27-Jun-2017 |
wenzelm <none@none> |
clarified defaults;
|
| #
3d4309c0 |
|
27-Jun-2017 |
wenzelm <none@none> |
tuned signature;
|
| #
4a4e793f |
|
13-Jun-2017 |
wenzelm <none@none> |
clarified modules;
|
| #
7dec135b |
|
14-Mar-2017 |
wenzelm <none@none> |
clarified singleton module;
|
| #
10701519 |
|
12-Mar-2017 |
wenzelm <none@none> |
tuned;
|
| #
e1c0d9f2 |
|
17-Jul-2015 |
wenzelm <none@none> |
tuned;
|
| #
40e642df |
|
23-Jul-2014 |
wenzelm <none@none> |
clarified module name: facilitate alternative GUI frameworks;
--HG--
rename : src/Pure/GUI/swing_thread.scala => src/Pure/GUI/gui_thread.scala
|
| #
7d07ee99 |
|
21-Jul-2014 |
wenzelm <none@none> |
proper Swing buttons instead of active areas within text (by Lars Hupel);
|
| #
023585e2 |
|
28-Apr-2014 |
wenzelm <none@none> |
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
|
| #
2ccf1463 |
|
24-Apr-2014 |
wenzelm <none@none> |
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
|
| #
da5844fe |
|
22-Apr-2014 |
wenzelm <none@none> |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
| #
e5bc4603 |
|
27-Mar-2014 |
wenzelm <none@none> |
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;
|
| #
d96a05b2 |
|
01-Mar-2014 |
wenzelm <none@none> |
tuned signature -- separate module Font_Info;
|
| #
d6d19c15 |
|
18-Feb-2014 |
wenzelm <none@none> |
tuned imports;
|
| #
6b0c03d3 |
|
04-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
--HG--
extra : amend_source : ecfd76d4e8277199ca35432e0682414689f265fb
|