| Wed, 28 Nov 2018 12:05:50 +0100 |
wenzelm |
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
|
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, 13 Jun 2017 20:16:39 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2017 21:43:54 +0100 |
wenzelm |
clarified singleton module;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 22:09:52 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2015 11:44:11 +0200 |
wenzelm |
maintain history more often;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 21:45:15 +0200 |
wenzelm |
more uniform ComponentAdapter;
|
file |
diff |
annotate
|
| Sun, 18 Jan 2015 17:32:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 14:13:38 +0100 |
wenzelm |
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
| Tue, 22 Jul 2014 13:36:51 +0200 |
wenzelm |
support multiple selected print operations instead of slightly odd "menu";
|
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
|
| Mon, 19 May 2014 15:23:08 +0200 |
wenzelm |
some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 21:14:25 +0200 |
wenzelm |
clarified detach_operation: ignore empty output;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 15:30:28 +0200 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 15:12:39 +0200 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 14:53:04 +0200 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 11:47:38 +0200 |
wenzelm |
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
|
file |
diff |
annotate
|
| Thu, 08 May 2014 00:14:06 +0200 |
wenzelm |
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
|
file |
diff |
annotate
|
| Tue, 06 May 2014 22:55:44 +0200 |
wenzelm |
tuned GUI layout;
|
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
|
| Tue, 06 May 2014 17:47:03 +0200 |
wenzelm |
clarified GUI focus;
|
file |
diff |
annotate
|
| Tue, 06 May 2014 17:28:58 +0200 |
wenzelm |
more uniform detach button;
|
file |
diff |
annotate
|
| Tue, 06 May 2014 16:57:17 +0200 |
wenzelm |
renamed "Find" to "Query", with more general operations;
|
file |
diff |
annotate
| base
|