# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1502485582 -7200
# Node ID 8c12f51d67ab3d8c90462eded237564949f49404
# Parent  4d2ce596f5050686df014a4c7a7d6d5d24742fea# Parent  f55d2e2c2ca050562dfcaa83da00132e8aa6a987
merged

diff -r 4d2ce596f505 -r 8c12f51d67ab src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Fri Aug 11 16:54:49 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json	Fri Aug 11 23:06:22 2017 +0200
@@ -10,7 +10,7 @@
         "document preparation"
     ],
     "icon": "isabelle.png",
-    "version": "0.22.0",
+    "version": "0.23.0",
     "publisher": "makarius",
     "license": "MIT",
     "repository": {
diff -r 4d2ce596f505 -r 8c12f51d67ab src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Aug 11 16:54:49 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Aug 11 23:06:22 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 4d2ce596f505 -r 8c12f51d67ab src/Tools/VSCode/extension/src/state_panel.ts
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Fri Aug 11 16:54:49 2017 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Fri Aug 11 23:06:22 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 })
diff -r 4d2ce596f505 -r 8c12f51d67ab src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Aug 11 16:54:49 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri Aug 11 23:06:22 2017 +0200
@@ -57,10 +57,12 @@
 
   /* query operation */
 
+  private val output_active = Synchronized(true)
+
   private val print_state =
     new Query_Operation(server.editor, (), "print_state", _ => (),
       (snapshot, results, body) =>
-        {
+        if (output_active.value) {
           val text = server.resources.output_pretty_message(Pretty.separate(body))
           val content =
             HTML.output_document(
@@ -160,8 +162,9 @@
 
   def exit()
   {
-    server.editor.send_wait_dispatcher { print_state.deactivate() }
+    output_active.change(_ => false)
     server.session.commands_changed -= main
     server.session.caret_focus -= main
+    server.editor.send_wait_dispatcher { print_state.deactivate() }
   }
 }