--- 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
)
--- 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",
--- 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(
--- 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<Dynamic_Output, void>("PIDE/dynamic_output")
+/* state */
+
+export interface State_Output
+{
+ id: number
+ content: string
+}
+
+export const state_output_type =
+ new NotificationType<State_Output, void>("PIDE/state_output")
+
+export interface State_Id
+{
+ id: number
+}
+
+export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
+export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
+export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
+export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
+
+
/* preview */
export interface Preview_Request
--- 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
--- 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")
--- /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
+ }
+}