obsolete;

--- a/src/Tools/VSCode/extension/src/state_panel.ts	Wed Feb 26 14:43:43 2020 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Wed Feb 26 14:47:36 2020 +0100
@@ -39,9 +39,7 @@
     this.webview_panel =
       window.createWebviewPanel("isabelle-state", "State", panel_column(),
         {
-          enableScripts: true,
-          enableCommandUris: true,
-          retainContextWhenHidden: true,
+          enableScripts: true
         });
     this.webview_panel.onDidDispose(exit_panel)
     this.webview_panel.webview.onDidReceiveMessage(message =>