--- 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() }
}
}