# HG changeset patch # User wenzelm # Date 1497639879 -7200 # Node ID 5aa9cb83e70e1634f62b36099e3e7d1e96590ee1 # Parent ee4c2d5b650ec5e15f405db193da5397ca3dd3b6 clarified modules; diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Pure/build-jars --- 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 ) diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/extension/src/extension.ts --- 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 */ diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/src/preview.scala --- 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) - } -} diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/src/preview_panel.scala --- /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) + } +} diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/src/server.scala --- 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") diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/src/state.scala --- 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 - } -} diff -r ee4c2d5b650e -r 5aa9cb83e70e src/Tools/VSCode/src/state_panel.scala --- /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 + } +}