--- a/src/Pure/build-jars Fri Jun 16 20:44:36 2017 +0200
+++ b/src/Pure/build-jars Fri Jun 16 21:04:39 2017 +0200
@@ -168,10 +168,10 @@
../Tools/VSCode/src/document_model.scala
../Tools/VSCode/src/dynamic_output.scala
../Tools/VSCode/src/grammar.scala
- ../Tools/VSCode/src/preview.scala
+ ../Tools/VSCode/src/preview_panel.scala
../Tools/VSCode/src/protocol.scala
../Tools/VSCode/src/server.scala
- ../Tools/VSCode/src/state.scala
+ ../Tools/VSCode/src/state_panel.scala
../Tools/VSCode/src/vscode_rendering.scala
../Tools/VSCode/src/vscode_resources.scala
)
--- a/src/Tools/VSCode/extension/src/extension.ts Fri Jun 16 20:44:36 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Jun 16 21:04:39 2017 +0200
@@ -4,9 +4,9 @@
import * as fs from 'fs';
import * as library from './library'
import * as decorations from './decorations';
-import * as preview from './preview';
+import * as preview_panel from './preview_panel';
import * as protocol from './protocol';
-import * as state from './state';
+import * as state_panel from './state_panel';
import * as symbol from './symbol';
import * as completion from './completion';
import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
@@ -102,25 +102,25 @@
})
- /* state */
+ /* state panel */
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))
+ 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))
- language_client.onReady().then(() => state.setup(context, language_client))
+ language_client.onReady().then(() => state_panel.setup(context, language_client))
- /* preview */
+ /* preview panel */
context.subscriptions.push(
- commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)),
- commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)),
- commands.registerCommand("isabelle.preview-source", preview.source),
- commands.registerCommand("isabelle.preview-update", preview.update))
+ commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
+ commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
+ commands.registerCommand("isabelle.preview-source", preview_panel.source),
+ commands.registerCommand("isabelle.preview-update", preview_panel.update))
- language_client.onReady().then(() => preview.setup(context, language_client))
+ language_client.onReady().then(() => preview_panel.setup(context, language_client))
/* Isabelle symbols */
--- a/src/Tools/VSCode/src/preview.scala Fri Jun 16 20:44:36 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-/* Title: Tools/VSCode/src/preview.scala
- Author: Makarius
-
-HTML document preview.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-import java.io.{File => JFile}
-
-
-class Preview(resources: VSCode_Resources)
-{
- private val pending = Synchronized(Map.empty[JFile, Int])
-
- def request(file: JFile, column: Int): Unit =
- pending.change(map => map + (file -> column))
-
- def flush(channel: Channel): Boolean =
- {
- pending.change_result(map =>
- {
- val map1 =
- (map /: map.iterator)({ case (m, (file, column)) =>
- resources.get_model(file) match {
- case Some(model) =>
- val snapshot = model.snapshot()
- if (snapshot.is_outdated) m
- else {
- val (label, content) = make_preview(model, snapshot)
- channel.write(Protocol.Preview_Response(file, column, label, content))
- m - file
- }
- case None => m - file
- }
- })
- (map1.nonEmpty, map1)
- })
- }
-
- def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
- {
- val label = "Preview " + quote(model.node_name.toString)
- val content =
- HTML.output_document(
- List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
- List(
- HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
- HTML.source(Present.theory_document(snapshot))),
- css = "")
- (label, content)
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Jun 16 21:04:39 2017 +0200
@@ -0,0 +1,56 @@
+/* Title: Tools/VSCode/src/preview_panel.scala
+ Author: Makarius
+
+HTML document preview.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+import java.io.{File => JFile}
+
+
+class Preview_Panel(resources: VSCode_Resources)
+{
+ private val pending = Synchronized(Map.empty[JFile, Int])
+
+ def request(file: JFile, column: Int): Unit =
+ pending.change(map => map + (file -> column))
+
+ def flush(channel: Channel): Boolean =
+ {
+ pending.change_result(map =>
+ {
+ val map1 =
+ (map /: map.iterator)({ case (m, (file, column)) =>
+ resources.get_model(file) match {
+ case Some(model) =>
+ val snapshot = model.snapshot()
+ if (snapshot.is_outdated) m
+ else {
+ val (label, content) = make_preview(model, snapshot)
+ channel.write(Protocol.Preview_Response(file, column, label, content))
+ m - file
+ }
+ case None => m - file
+ }
+ })
+ (map1.nonEmpty, map1)
+ })
+ }
+
+ def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
+ {
+ val label = "Preview " + quote(model.node_name.toString)
+ val content =
+ HTML.output_document(
+ List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
+ List(
+ HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
+ HTML.source(Present.theory_document(snapshot))),
+ css = "")
+ (label, content)
+ }
+}
--- a/src/Tools/VSCode/src/server.scala Fri Jun 16 20:44:36 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Fri Jun 16 21:04:39 2017 +0200
@@ -181,17 +181,17 @@
/* preview */
- private lazy val preview = new Preview(resources)
+ private lazy val preview_panel = new Preview_Panel(resources)
private lazy val delay_preview: Standard_Thread.Delay =
Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
- if (preview.flush(channel)) delay_preview.invoke()
+ if (preview_panel.flush(channel)) delay_preview.invoke()
}
private def request_preview(file: JFile, column: Int)
{
- preview.request(file, column)
+ preview_panel.request(file, column)
delay_preview.invoke()
}
@@ -400,10 +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.State_Init(()) => State_Panel.init(server)
+ case Protocol.State_Exit(id) => State_Panel.exit(id)
+ case Protocol.State_Locate(id) => State_Panel.locate(id)
+ case Protocol.State_Update(id) => State_Panel.update(id)
case Protocol.Preview_Request(file, column) => request_preview(file, column)
case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
case _ => log("### IGNORED")
--- a/src/Tools/VSCode/src/state.scala Fri Jun 16 20:44:36 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-/* 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
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/state_panel.scala Fri Jun 16 21:04:39 2017 +0200
@@ -0,0 +1,118 @@
+/* Title: Tools/VSCode/src/state_panel.scala
+ Author: Makarius
+
+Show proof state.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object State_Panel
+{
+ private val make_id = Counter.make()
+ private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
+
+ def init(server: Server)
+ {
+ val instance = new State_Panel(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_Panel private(val server: Server)
+{
+ /* output */
+
+ val id: Counter.ID = State_Panel.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
+ }
+}