src/Tools/jEdit/src/query_dockable.scala
Tue, 14 Mar 2017 21:43:54 +0100 wenzelm clarified singleton module;
Mon, 05 Sep 2016 22:09:52 +0200 wenzelm clarified modules;
Fri, 07 Aug 2015 11:44:11 +0200 wenzelm maintain history more often;
Fri, 17 Jul 2015 21:45:15 +0200 wenzelm more uniform ComponentAdapter;
Sun, 18 Jan 2015 17:32:38 +0100 wenzelm tuned;
Mon, 05 Jan 2015 14:13:38 +0100 wenzelm GUI.imitate_font: more explicit result size, e.g. relevant for caching;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Tue, 22 Jul 2014 13:36:51 +0200 wenzelm support multiple selected print operations instead of slightly odd "menu";
Wed, 21 May 2014 16:21:11 +0200 wenzelm more uniform Font_Info.Zoom_Box;
Wed, 21 May 2014 14:42:45 +0200 wenzelm tuned signature;
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;
Thu, 08 May 2014 21:14:25 +0200 wenzelm clarified detach_operation: ignore empty output;
Thu, 08 May 2014 15:30:28 +0200 wenzelm tuned GUI;
Thu, 08 May 2014 15:12:39 +0200 wenzelm tuned GUI;
Thu, 08 May 2014 14:53:04 +0200 wenzelm tuned GUI;
Thu, 08 May 2014 11:47:38 +0200 wenzelm enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
Thu, 08 May 2014 00:14:06 +0200 wenzelm some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
Tue, 06 May 2014 22:55:44 +0200 wenzelm tuned GUI layout;
Tue, 06 May 2014 21:29:17 +0200 wenzelm common support for search field, which is actually a light-weight Highlighter;
Tue, 06 May 2014 17:47:03 +0200 wenzelm clarified GUI focus;
Tue, 06 May 2014 17:28:58 +0200 wenzelm more uniform detach button;
Tue, 06 May 2014 16:57:17 +0200 wenzelm renamed "Find" to "Query", with more general operations;
less more (0) tip