# HG changeset patch
# User wenzelm
# Date 1502467726 -7200
# Node ID 14146fb264d8553e9ebd9b32c814a921a11fe245
# Parent  32084d7e6b598414e500e03f89ed6dbad450c3dd
proper state_panel exit;

diff -r 32084d7e6b59 -r 14146fb264d8 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Aug 11 14:29:30 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Aug 11 18:08:46 2017 +0200
@@ -129,7 +129,8 @@
       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))
+      commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update),
+      workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri)))
 
     language_client.onReady().then(() => state_panel.setup(context, language_client))
 
diff -r 32084d7e6b59 -r 14146fb264d8 src/Tools/VSCode/extension/src/state_panel.ts
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Fri Aug 11 14:29:30 2017 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Fri Aug 11 18:08:46 2017 +0200
@@ -67,6 +67,12 @@
   if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
 }
 
+export function exit_uri(uri: Uri)
+{
+  const id = decode_state(uri)
+  if (id) exit(id)
+}
+
 export function locate(id: number)
 {
   if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })