Fri, 08 Nov 2024 13:27:26 +0100 |
wenzelm |
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
|
file |
diff |
annotate
|
Thu, 07 Nov 2024 13:22:59 +0100 |
wenzelm |
more uniform pretty_text_area.zoom via its zoom_component;
|
file |
diff |
annotate
|
Wed, 06 Nov 2024 22:04:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 08 Dec 2022 22:38:03 +0100 |
wenzelm |
clarified signature: proper scopes and types;
|
file |
diff |
annotate
|
Sat, 13 Aug 2022 12:32:38 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
Fri, 12 Aug 2022 12:12:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 12 Aug 2022 12:06:29 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 12 Aug 2022 11:47:12 +0200 |
wenzelm |
tuned, following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
Fri, 12 Aug 2022 11:35:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
Thu, 15 Jul 2021 16:35:45 +0200 |
wenzelm |
build.props for isabelle.jar, including isabelle.jedit;
|
file |
diff |
annotate
|
Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
Mon, 06 Apr 2020 12:53:45 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 01 Sep 2017 15:15:29 +0200 |
wenzelm |
more robust: provide docking framework via base plugin;
|
file |
diff |
annotate
|
Tue, 27 Jun 2017 21:56:56 +0200 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
Tue, 27 Jun 2017 21:36:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 10 Jan 2017 16:03:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 17 Jul 2015 21:45:15 +0200 |
wenzelm |
more uniform ComponentAdapter;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
Wed, 21 May 2014 16:21:11 +0200 |
wenzelm |
more uniform Font_Info.Zoom_Box;
|
file |
diff |
annotate
|
Wed, 21 May 2014 14:42:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 06 May 2014 21:29:17 +0200 |
wenzelm |
common support for search field, which is actually a light-weight Highlighter;
|
file |
diff |
annotate
|
Fri, 25 Apr 2014 12:51:08 +0200 |
wenzelm |
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
|
file |
diff |
annotate
|
Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 19:39:27 +0100 |
wenzelm |
tuned signature -- separate module Font_Info;
|
file |
diff |
annotate
|
Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 15:50:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 15:09:15 +0200 |
wenzelm |
improved FlowLayout for wrapping of components over multiple lines;
|
file |
diff |
annotate
|
Sat, 24 Aug 2013 13:32:51 +0200 |
wenzelm |
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
|
file |
diff |
annotate
|
Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 08 Aug 2013 14:13:04 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
Thu, 04 Apr 2013 17:58:47 +0200 |
wenzelm |
tuned signature -- concentrate GUI tools;
|
file |
diff |
annotate
|
Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
Mon, 10 Dec 2012 15:13:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 21:23:20 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 21:10:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 18 Nov 2012 15:28:58 +0100 |
wenzelm |
update options via protocol;
|
file |
diff |
annotate
|
Tue, 16 Oct 2012 22:13:46 +0200 |
wenzelm |
retain info dockable state via educated guess on window focus;
|
file |
diff |
annotate
|
Sun, 07 Oct 2012 16:05:31 +0200 |
wenzelm |
detach tooltip as dockable window;
|
file |
diff |
annotate
|