# HG changeset patch # User Lars Hupel # 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() } } }