# HG changeset patch # User wenzelm # Date 1497622877 -7200 # Node ID 6187612e83c134708c06656bf1472464ef69c239 # Parent 78a1aedd1761a20b3ef64787c6ebc68837348cbd support for separate proof state output; diff -r 78a1aedd1761 -r 6187612e83c1 src/Pure/build-jars --- a/src/Pure/build-jars Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Pure/build-jars Fri Jun 16 16:21:17 2017 +0200 @@ -171,6 +171,7 @@ ../Tools/VSCode/src/preview.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala + ../Tools/VSCode/src/state.scala ../Tools/VSCode/src/vscode_rendering.scala ../Tools/VSCode/src/vscode_resources.scala ) diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Fri Jun 16 16:21:17 2017 +0200 @@ -33,6 +33,11 @@ "contributes": { "commands": [ { + "command": "isabelle.state", + "title": "Show Proof State", + "category": "Isabelle" + }, + { "command": "isabelle.preview", "title": "Open Preview", "category": "Isabelle", diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Fri Jun 16 16:21:17 2017 +0200 @@ -6,6 +6,7 @@ import * as decorations from './decorations'; import * as preview from './preview'; import * as protocol from './protocol'; +import * as state from './state'; import * as symbol from './symbol'; import * as completion from './completion'; import { ExtensionContext, workspace, window, commands, languages } from 'vscode'; @@ -101,6 +102,16 @@ }) + /* state */ + + context.subscriptions.push( + commands.registerCommand("isabelle.state", uri => state.init(uri)), + commands.registerCommand("_isabelle.state-locate", state.locate), + commands.registerCommand("_isabelle.state-update", state.update)) + + language_client.onReady().then(() => state.setup(context, language_client)) + + /* preview */ context.subscriptions.push( diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/extension/src/protocol.ts --- a/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 16 16:21:17 2017 +0200 @@ -47,6 +47,28 @@ new NotificationType("PIDE/dynamic_output") +/* state */ + +export interface State_Output +{ + id: number + content: string +} + +export const state_output_type = + new NotificationType("PIDE/state_output") + +export interface State_Id +{ + id: number +} + +export const state_init_type = new NotificationType("PIDE/state_init") +export const state_exit_type = new NotificationType("PIDE/state_exit") +export const state_locate_type = new NotificationType("PIDE/state_locate") +export const state_update_type = new NotificationType("PIDE/state_update") + + /* preview */ export interface Preview_Request diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Fri Jun 16 16:21:17 2017 +0200 @@ -467,6 +467,29 @@ } + /* state output */ + + object State_Output + { + def apply(id: Counter.ID, content: String): JSON.T = + Notification("PIDE/state_output", Map("id" -> id, "content" -> content)) + } + + class State_Id_Notification(name: String) + { + def unapply(json: JSON.T): Option[Counter.ID] = + json match { + case Notification(method, Some(params)) if method == name => JSON.long(params, "id") + case _ => None + } + } + + object State_Init extends Notification0("PIDE/state_init") + object State_Exit extends State_Id_Notification("PIDE/state_exit") + object State_Locate extends State_Id_Notification("PIDE/state_locate") + object State_Update extends State_Id_Notification("PIDE/state_update") + + /* preview */ object Preview_Request diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Fri Jun 16 16:21:17 2017 +0200 @@ -400,6 +400,10 @@ case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) + case Protocol.State_Init(()) => State.init(server) + case Protocol.State_Exit(id) => State.exit(id) + case Protocol.State_Locate(id) => State.locate(id) + case Protocol.State_Update(id) => State.update(id) case Protocol.Preview_Request(file, column) => request_preview(file, column) case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) case _ => log("### IGNORED") diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/src/state.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/state.scala Fri Jun 16 16:21:17 2017 +0200 @@ -0,0 +1,118 @@ +/* Title: Tools/VSCode/src/state.scala + Author: Makarius + +Show proof state. +*/ + +package isabelle.vscode + + +import isabelle._ + + +object State +{ + private val make_id = Counter.make() + private val instances = Synchronized(Map.empty[Counter.ID, State]) + + def init(server: Server) + { + val instance = new State(server) + instances.change(_ + (instance.id -> instance)) + instance.init() + } + + def exit(id: Counter.ID) + { + instances.change(map => + map.get(id) match { + case None => map + case Some(instance) => instance.exit(); map - id + }) + } + + def locate(id: Counter.ID): Unit = + instances.value.get(id).foreach(state => + state.server.editor.send_dispatcher(state.locate())) + + def update(id: Counter.ID): Unit = + instances.value.get(id).foreach(state => + state.server.editor.send_dispatcher(state.update())) +} + + +class State private(val server: Server) +{ + /* output */ + + val id: Counter.ID = State.make_id() + + private def output(content: String): Unit = + server.channel.write(Protocol.State_Output(id, content)) + + + /* query operation */ + + private val print_state = + new Query_Operation(server.editor, (), "print_state", _ => (), + (snapshot, results, body) => + { + val text = server.resources.output_pretty_message(Pretty.separate(body)) + val content = + HTML.output_document( + List(HTML.style(HTML.fonts_css()), + HTML.style_file(Url.print_file(HTML.isabelle_css.file))), + List( + HTML.chapter("Proof state"), + HTML.source(text)), + css = "") + output(content) + }) + + def locate() { print_state.locate_query() } + + def update() + { + server.editor.current_node_snapshot(()) match { + case Some(snapshot) => + (server.editor.current_command((), snapshot), print_state.get_location) match { + case (Some(command1), Some(command2)) if command1.id == command2.id => + case _ => print_state.apply_query(Nil) + } + case None => + } + } + + + /* auto update */ + + private val auto_update_enabled = Synchronized(true) + + def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() } + + def auto_update(): Unit = if (auto_update_enabled.value) update() + + + /* main */ + + private val main = + Session.Consumer[Any](getClass.getName) { + case changed: Session.Commands_Changed => if (changed.assignment) auto_update() + case Session.Caret_Focus => auto_update() + } + + def init() + { + server.session.commands_changed += main + server.session.caret_focus += main + server.editor.send_wait_dispatcher { print_state.activate() } + server.editor.send_dispatcher { auto_update() } + } + + def exit() + { + server.editor.send_wait_dispatcher { print_state.deactivate() } + server.session.commands_changed -= main + server.session.caret_focus -= main + } +}