# HG changeset patch
# User wenzelm
# Date 1502471382 -7200
# Node ID f55d2e2c2ca050562dfcaa83da00132e8aa6a987
# Parent  29717b0a1ab33d4a8329e6a4f7a2d288514bba8c
avoid spurious output after exit;

diff -r 29717b0a1ab3 -r f55d2e2c2ca0 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Aug 11 18:51:25 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri Aug 11 19:09:42 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() }
   }
 }