# HG changeset patch
# User wenzelm
# Date 1582724856 -3600
# Node ID 24e3adaee6ec094cb5ec05fc0660e341a97c02e8
# Parent  ecefde4f910387684fcfffc677eb957c0da3e682
obsolete;

diff -r ecefde4f9103 -r 24e3adaee6ec src/Tools/VSCode/extension/src/state_panel.ts
--- 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 =>