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 |