clarified Panel;
discontinued intermediate Content_Provider;

--- a/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 25 19:20:21 2020 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 25 21:28:06 2020 +0100
@@ -133,8 +133,7 @@
       commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
       commands.registerCommand("_isabelle.state-locate", state_panel.locate),
       commands.registerCommand("_isabelle.state-update", state_panel.update),
-      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update),
-      workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri)))
+      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update))
 
     language_client.onReady().then(() => state_panel.setup(context, language_client))
 

--- a/src/Tools/VSCode/extension/src/state_panel.ts	Tue Feb 25 19:20:21 2020 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Tue Feb 25 21:28:06 2020 +0100
@@ -4,88 +4,98 @@
 import * as protocol from './protocol'
 import { Content_Provider } from './content_provider'
 import { LanguageClient, VersionedTextDocumentIdentifier } from 'vscode-languageclient';
-import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel } from 'vscode'
+import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel, ViewColumn } from 'vscode'
+import { create } from 'domain';
 
 
-/* HTML content */
+let language_client: LanguageClient
 
-const content_provider = new Content_Provider("isabelle-state")
-
-function encode_state(id: number | undefined): Uri | undefined
+class Panel
 {
-  return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined
-}
+  private state_id: number
+  private webview_panel: WebviewPanel
+
+  public get_id(): number { return this.state_id}
+  public check_id(id: number): boolean { return this.state_id == id }
+
+  public set_content(id: number, html: string)
+  {
+    this.state_id = id
+    this.webview_panel.webview.html = html
+  }
 
-function decode_state(uri: Uri | undefined): number | undefined
-{
-  if (uri && uri.scheme === content_provider.uri_scheme) {
-    const id = parseInt(uri.fragment)
-    return id ? id : undefined
+  constructor(column: ViewColumn)
+  {
+    this.webview_panel =
+      window.createWebviewPanel("isabelle-state", "State", column,
+        {
+          enableScripts: true,
+          enableCommandUris: true,
+          retainContextWhenHidden: true,
+        });
+    this.webview_panel.onDidDispose(exit_panel)
   }
-  else undefined
+
+  public locate()
+  {
+    language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+  }
+
+  public update()
+  {
+    language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+  }
+
+  public auto_update(enabled: boolean)
+  {
+    language_client.sendNotification(
+    protocol.state_auto_update_type, { id: this.state_id, enabled: enabled })
+  }
 }
 
 
-/* setup */
+/* global panel */
+
+let panel: Panel
 
-let language_client: LanguageClient
+function check_panel(id: number): boolean
+{
+  return panel && panel.check_id(id)
+}
+
+function exit_panel()
+{
+  if (panel) {
+    language_client.sendNotification(protocol.state_exit_type, { id: panel.get_id() })
+    panel = null
+  }
+}
 
 export function setup(context: ExtensionContext, client: LanguageClient)
 {
-  context.subscriptions.push(content_provider.register())
-
-  var panel: WebviewPanel
   language_client = client
   language_client.onNotification(protocol.state_output_type, params =>
     {
-      const uri = encode_state(params.id)
       if (!panel) {
         const column = library.adjacent_editor_column(window.activeTextEditor, true)
-        panel = window.createWebviewPanel(
-          uri.fsPath,
-          "State",
-          column,
-          {
-            enableScripts: true,
-            retainContextWhenHidden: true
-          }
-        );
+        panel = new Panel(column)
       }
-      panel.webview.html = params.content;
+      panel.set_content(params.id, params.content)
     })
 }
 
 
 /* commands */
 
-export function init(uri: Uri)
-{
-  if (language_client) language_client.sendNotification(protocol.state_init_type)
-}
-
-export function exit(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
+export function init(uri: Uri) {
+  language_client.sendNotification(protocol.state_init_type)
 }
 
-export function exit_uri(uri: Uri)
-{
-  const id = decode_state(uri)
-  if (id) exit(id)
-}
+export function locate(id: number) { if (check_panel(id)) panel.locate() }
 
-export function locate(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
-}
-
-export function update(id: number)
-{
-  if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
-}
+export function update(id: number) { if (check_panel(id)) panel.update() }
 
 export function auto_update(id: number, enabled: boolean)
 {
-  if (language_client)
-    language_client.sendNotification(protocol.state_auto_update_type, { id: id, enabled: enabled })
+  if (check_panel(id)) { panel.auto_update(enabled) }
 }