--- 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": {
--- 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))
--- 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 })
--- 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() }
}
}