src/Tools/VSCode/extension/src/state_panel.ts
Wed, 26 Feb 2020 14:47:36 +0100 wenzelm obsolete;
Wed, 26 Feb 2020 14:43:43 +0100 wenzelm proper message passing -- discontinued obsolete auxiliary commands;
Tue, 25 Feb 2020 21:28:06 +0100 wenzelm clarified Panel;
Tue, 25 Feb 2020 18:30:08 +0100 wenzelm update to WebviewPanel API, following initial version by Peter Zeller;
Fri, 11 Aug 2017 18:08:46 +0200 wenzelm proper state_panel exit;
Thu, 29 Jun 2017 11:36:25 +0200 wenzelm HTML GUI actions via JavaScript;
Tue, 27 Jun 2017 16:50:40 +0200 wenzelm added missing files (cf. 5aa9cb83e70e);
less more (0) tip