src/Tools/VSCode/src/state_panel.scala
Fri, 11 Aug 2017 19:09:42 +0200 wenzelm avoid spurious output after exit;
Thu, 29 Jun 2017 11:58:00 +0200 wenzelm proper dynamic controls, notably for auto_update_enabled;
Thu, 29 Jun 2017 11:42:42 +0200 wenzelm tuned signature;
Thu, 29 Jun 2017 11:36:25 +0200 wenzelm HTML GUI actions via JavaScript;
Tue, 27 Jun 2017 21:56:56 +0200 wenzelm clarified defaults;
Tue, 27 Jun 2017 11:49:47 +0200 wenzelm GUI controls similar to Tools/jEdit/src/state_dockable.scala;
Fri, 16 Jun 2017 22:38:19 +0200 wenzelm tuned;
Fri, 16 Jun 2017 21:04:39 +0200 wenzelm clarified modules;
less more (0) tip