--- a/src/Tools/VSCode/extension/src/extension.ts Fri Aug 11 14:29:30 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Aug 11 18:08:46 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 14:29:30 2017 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Fri Aug 11 18:08:46 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 })