proper state_panel exit;
authorwenzelm
Fri, 11 Aug 2017 18:08:46 +0200
changeset 66395 14146fb264d8
parent 66394 32084d7e6b59
child 66396 29717b0a1ab3
proper state_panel exit;
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/state_panel.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))
 
--- 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 })