| author | wenzelm |
| Sat, 17 Jun 2017 14:52:23 +0200 | |
| changeset 66103 | 8ff7fd4ee919 |
| parent 66089 | def95e0bc529 (current diff) |
| parent 66102 | 3e2145cf3077 (diff) |
| child 66104 | 5aab14a64a03 |
| child 66109 | e034a563ed7d |
| src/Tools/VSCode/src/preview.scala | file | annotate | diff | comparison | revisions |
--- a/src/Pure/Concurrent/consumer_thread.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/Concurrent/consumer_thread.scala Sat Jun 17 14:52:23 2017 +0200 @@ -33,6 +33,7 @@ private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) } def is_active: Boolean = active && thread.isAlive + def check_thread: Boolean = Thread.currentThread == thread private def failure(exn: Throwable): Unit = Output.error_message(
--- a/src/Pure/GUI/gui_thread.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/GUI/gui_thread.scala Sat Jun 17 14:52:23 2017 +0200 @@ -14,13 +14,13 @@ { /* context check */ - def assert[A](body: => A) = + def assert[A](body: => A): A = { Predef.assert(SwingUtilities.isEventDispatchThread()) body } - def require[A](body: => A) = + def require[A](body: => A): A = { Predef.require(SwingUtilities.isEventDispatchThread()) body
--- a/src/Pure/PIDE/editor.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/PIDE/editor.scala Sat Jun 17 14:52:23 2017 +0200 @@ -14,6 +14,10 @@ def session: Session def flush(): Unit def invoke(): Unit + + + /* current situation */ + def current_node(context: Context): Option[Document.Node.Name] def current_node_snapshot(context: Context): Option[Document.Snapshot] def node_snapshot(name: Document.Node.Name): Document.Snapshot @@ -22,16 +26,9 @@ /* overlays */ - private val overlays = Synchronized(Document.Overlays.empty) - - def node_overlays(name: Document.Node.Name): Document.Node.Overlays = - overlays.value(name) - - def insert_overlay(command: Command, fn: String, args: List[String]): Unit = - overlays.change(_.insert(command, fn, args)) - - def remove_overlay(command: Command, fn: String, args: List[String]): Unit = - overlays.change(_.remove(command, fn, args)) + def node_overlays(name: Document.Node.Name): Document.Node.Overlays + def insert_overlay(command: Command, fn: String, args: List[String]) + def remove_overlay(command: Command, fn: String, args: List[String]) /* hyperlinks */ @@ -45,4 +42,12 @@ def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) : Option[Hyperlink] + + + /* dispatcher thread */ + + def assert_dispatcher[A](body: => A): A + def require_dispatcher[A](body: => A): A + def send_dispatcher(body: => Unit): Unit + def send_wait_dispatcher(body: => Unit): Unit }
--- a/src/Pure/PIDE/query_operation.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/PIDE/query_operation.scala Sat Jun 17 14:52:23 2017 +0200 @@ -48,7 +48,7 @@ private val print_function = operation_name + "_query" - /* implicit state -- owned by GUI thread */ + /* implicit state -- owned by editor thread */ private val current_state = Synchronized(Query_Operation.State.empty) @@ -67,7 +67,7 @@ private def content_update() { - GUI_Thread.require {} + editor.require_dispatcher {} /* snapshot */ @@ -174,11 +174,11 @@ /* query operations */ def cancel_query(): Unit = - GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) } + editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) } def apply_query(query: List[String]) { - GUI_Thread.require {} + editor.require_dispatcher {} editor.current_node_snapshot(editor_context) match { case Some(snapshot) => @@ -202,7 +202,7 @@ def locate_query() { - GUI_Thread.require {} + editor.require_dispatcher {} val state = current_state.value for { @@ -224,7 +224,7 @@ if state.update_pending || (state.status != Query_Operation.Status.FINISHED && changed.commands.contains(command)) => - GUI_Thread.later { content_update() } + editor.send_dispatcher { content_update() } case _ => } }
--- a/src/Pure/PIDE/session.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/PIDE/session.scala Sat Jun 17 14:52:23 2017 +0200 @@ -136,11 +136,38 @@ def reparse_limit: Int = session_options.int("editor_reparse_limit") - /* outlets */ + /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } + def assert_dispatcher[A](body: => A): A = + { + assert(dispatcher.check_thread) + body + } + + def require_dispatcher[A](body: => A): A = + { + require(dispatcher.check_thread) + body + } + + def send_dispatcher(body: => Unit): Unit = + { + if (dispatcher.check_thread) body + else dispatcher.send(() => body) + } + + def send_wait_dispatcher(body: => Unit): Unit = + { + if (dispatcher.check_thread) body + else dispatcher.send_wait(() => body) + } + + + /* outlets */ + val statistics = new Session.Outlet[Session.Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
--- a/src/Pure/build-jars Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Pure/build-jars Sat Jun 17 14:52:23 2017 +0200 @@ -168,9 +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_panel.scala ../Tools/VSCode/src/vscode_rendering.scala ../Tools/VSCode/src/vscode_resources.scala )
--- a/src/Tools/VSCode/extension/package.json Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Sat Jun 17 14:52:23 2017 +0200 @@ -8,14 +8,20 @@ "mathematical logic", "functional programming", "document preparation" - ], + ], "icon": "isabelle.png", - "version": "0.14.0", + "version": "0.15.0", "publisher": "makarius", "license": "MIT", - "repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" }, - "engines": { "vscode": "^1.8.0" }, - "categories": ["Languages"], + "repository": { + "url": "http://isabelle.in.tum.de/repos/isabelle" + }, + "engines": { + "vscode": "^1.8.0" + }, + "categories": [ + "Languages" + ], "activationEvents": [ "onLanguage:isabelle", "onLanguage:isabelle-ml", @@ -27,6 +33,11 @@ "contributes": { "commands": [ { + "command": "isabelle.state", + "title": "Show Proof State", + "category": "Isabelle" + }, + { "command": "isabelle.preview", "title": "Open Preview", "category": "Isabelle", @@ -97,17 +108,26 @@ "languages": [ { "id": "isabelle", - "aliases": ["Isabelle"], - "extensions": [".thy"], + "aliases": [ + "Isabelle" + ], + "extensions": [ + ".thy" + ], "configuration": "./isabelle-language.json" }, { "id": "isabelle-ml", - "aliases": ["Isabelle/ML"], - "extensions": [".ML", ".sml", ".sig"], + "aliases": [ + "Isabelle/ML" + ], + "extensions": [ + ".ML", + ".sml", + ".sig" + ], "configuration": "./isabelle-ml-language.json" } - ], "grammars": [ { @@ -131,7 +151,9 @@ }, "isabelle.args": { "type": "array", - "items": { "type": "string" }, + "items": { + "type": "string" + }, "default": [], "description": "Command-line arguments for isabelle vscode_server process." }, @@ -140,80 +162,302 @@ "default": "", "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)." }, - "isabelle.unprocessed_light_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" }, - "isabelle.unprocessed_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" }, - "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, - "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" }, - "isabelle.running_light_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" }, - "isabelle.running_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" }, - "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" }, - "isabelle.running1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.40)" }, - "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.40)" }, - "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(204, 136, 0, 0.20)" }, - "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" }, - "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(5, 199, 5, 0.20)" }, - "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" }, - "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(204, 143, 0, 0.20)" }, - "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, - "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(0, 0, 204, 0.20)" }, - "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, - "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(204, 0, 105, 0.20)" }, - "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" }, - "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(150, 150, 150, 0.15)" }, - "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }, - "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 214, 102, 0.15)" }, - "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" }, - "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" }, - "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, - "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, - "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, - "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, - "isabelle.error_light_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" }, - "isabelle.error_dark_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" }, - "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, - "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, - "isabelle.main_light_color": { "type": "string", "default": "rgba(0, 0, 0, 1.00)" }, - "isabelle.main_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" }, - "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(175, 0, 219, 1.00)" }, - "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }, - "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, - "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, - "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(38, 127, 153, 1.00)" }, - "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(78, 201, 176), 1.00)" }, - "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, - "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, - "isabelle.improper_light_color": { "type": "string", "default": "rgba(205, 49, 49, 1.00)" }, - "isabelle.improper_dark_color": { "type": "string", "default": "rgba(244, 71, 71, 1.00)" }, - "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, - "isabelle.operator_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" }, - "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, - "isabelle.free_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, - "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.bound_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, - "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 16, 128, 1.00)" }, - "isabelle.var_dark_color": { "type": "string", "default": "rgba(156, 220, 254, 1.00)" }, - "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, - "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, - "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(163, 21, 21, 1.00)" }, - "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(206, 145, 120, 1.00)" }, - "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" }, - "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" }, - "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, - "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(121, 94, 38, 1.00)" }, - "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(220, 220, 170, 1.00)" }, - "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, - "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" } + "isabelle.unprocessed_light_color": { + "type": "string", + "default": "rgba(255, 160, 160, 1.00)" + }, + "isabelle.unprocessed_dark_color": { + "type": "string", + "default": "rgba(97, 0, 97, 1.00)" + }, + "isabelle.unprocessed1_light_color": { + "type": "string", + "default": "rgba(255, 160, 160, 0.20)" + }, + "isabelle.unprocessed1_dark_color": { + "type": "string", + "default": "rgba(97, 0, 97, 0.20)" + }, + "isabelle.running_light_color": { + "type": "string", + "default": "rgba(97, 0, 97, 1.00)" + }, + "isabelle.running_dark_color": { + "type": "string", + "default": "rgba(255, 160, 160, 1.00)" + }, + "isabelle.running1_light_color": { + "type": "string", + "default": "rgba(97, 0, 97, 0.40)" + }, + "isabelle.running1_dark_color": { + "type": "string", + "default": "rgba(255, 160, 160, 0.40)" + }, + "isabelle.bad_light_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.bad_dark_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.intensify_light_color": { + "type": "string", + "default": "rgba(255, 204, 102, 0.40)" + }, + "isabelle.intensify_dark_color": { + "type": "string", + "default": "rgba(204, 136, 0, 0.20)" + }, + "isabelle.markdown_item1_light_color": { + "type": "string", + "default": "rgba(218, 254, 218, 1.00)" + }, + "isabelle.markdown_item1_dark_color": { + "type": "string", + "default": "rgba(5, 199, 5, 0.20)" + }, + "isabelle.markdown_item2_light_color": { + "type": "string", + "default": "rgba(255, 240, 204, 1.00)" + }, + "isabelle.markdown_item2_dark_color": { + "type": "string", + "default": "rgba(204, 143, 0, 0.20)" + }, + "isabelle.markdown_item3_light_color": { + "type": "string", + "default": "rgba(231, 231, 255, 1.00)" + }, + "isabelle.markdown_item3_dark_color": { + "type": "string", + "default": "rgba(0, 0, 204, 0.20)" + }, + "isabelle.markdown_item4_light_color": { + "type": "string", + "default": "rgba(255, 224, 240, 1.00)" + }, + "isabelle.markdown_item4_dark_color": { + "type": "string", + "default": "rgba(204, 0, 105, 0.20)" + }, + "isabelle.quoted_light_color": { + "type": "string", + "default": "rgba(139, 139, 139, 0.10)" + }, + "isabelle.quoted_dark_color": { + "type": "string", + "default": "rgba(150, 150, 150, 0.15)" + }, + "isabelle.antiquoted_light_color": { + "type": "string", + "default": "rgba(255, 200, 50, 0.10)" + }, + "isabelle.antiquoted_dark_color": { + "type": "string", + "default": "rgba(255, 214, 102, 0.15)" + }, + "isabelle.writeln_light_color": { + "type": "string", + "default": "rgba(192, 192, 192, 1.0)" + }, + "isabelle.writeln_dark_color": { + "type": "string", + "default": "rgba(192, 192, 192, 1.0)" + }, + "isabelle.information_light_color": { + "type": "string", + "default": "rgba(193, 223, 238, 1.0)" + }, + "isabelle.information_dark_color": { + "type": "string", + "default": "rgba(193, 223, 238, 1.0)" + }, + "isabelle.warning_light_color": { + "type": "string", + "default": "rgba(255, 140, 0, 1.0)" + }, + "isabelle.warning_dark_color": { + "type": "string", + "default": "rgba(255, 140, 0, 1.0)" + }, + "isabelle.error_light_color": { + "type": "string", + "default": "rgba(178, 34, 34, 1.00)" + }, + "isabelle.error_dark_color": { + "type": "string", + "default": "rgba(178, 34, 34, 1.00)" + }, + "isabelle.spell_checker_light_color": { + "type": "string", + "default": "rgba(0, 0, 255, 1.0)" + }, + "isabelle.spell_checker_dark_color": { + "type": "string", + "default": "rgba(86, 156, 214, 1.00)" + }, + "isabelle.main_light_color": { + "type": "string", + "default": "rgba(0, 0, 0, 1.00)" + }, + "isabelle.main_dark_color": { + "type": "string", + "default": "rgba(212, 212, 212, 1.00)" + }, + "isabelle.keyword1_light_color": { + "type": "string", + "default": "rgba(175, 0, 219, 1.00)" + }, + "isabelle.keyword1_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + }, + "isabelle.keyword2_light_color": { + "type": "string", + "default": "rgba(9, 136, 90, 1.00)" + }, + "isabelle.keyword2_dark_color": { + "type": "string", + "default": "rgba(181, 206, 168, 1.00)" + }, + "isabelle.keyword3_light_color": { + "type": "string", + "default": "rgba(38, 127, 153, 1.00)" + }, + "isabelle.keyword3_dark_color": { + "type": "string", + "default": "rgba(78, 201, 176), 1.00)" + }, + "isabelle.quasi_keyword_light_color": { + "type": "string", + "default": "rgba(153, 102, 255, 1.00)" + }, + "isabelle.quasi_keyword_dark_color": { + "type": "string", + "default": "rgba(153, 102, 255, 1.00)" + }, + "isabelle.improper_light_color": { + "type": "string", + "default": "rgba(205, 49, 49, 1.00)" + }, + "isabelle.improper_dark_color": { + "type": "string", + "default": "rgba(244, 71, 71, 1.00)" + }, + "isabelle.operator_light_color": { + "type": "string", + "default": "rgba(50, 50, 50, 1.00)" + }, + "isabelle.operator_dark_color": { + "type": "string", + "default": "rgba(212, 212, 212, 1.00)" + }, + "isabelle.tfree_light_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tfree_dark_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tvar_light_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tvar_dark_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.free_light_color": { + "type": "string", + "default": "rgba(0, 0, 255, 1.00)" + }, + "isabelle.free_dark_color": { + "type": "string", + "default": "rgba(86, 156, 214, 1.00)" + }, + "isabelle.skolem_light_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.skolem_dark_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.bound_light_color": { + "type": "string", + "default": "rgba(0, 128, 0, 1.00)" + }, + "isabelle.bound_dark_color": { + "type": "string", + "default": "rgba(96, 139, 78, 1.00)" + }, + "isabelle.var_light_color": { + "type": "string", + "default": "rgba(0, 16, 128, 1.00)" + }, + "isabelle.var_dark_color": { + "type": "string", + "default": "rgba(156, 220, 254, 1.00)" + }, + "isabelle.inner_numeral_light_color": { + "type": "string", + "default": "rgba(9, 136, 90, 1.00)" + }, + "isabelle.inner_numeral_dark_color": { + "type": "string", + "default": "rgba(181, 206, 168, 1.00)" + }, + "isabelle.inner_quoted_light_color": { + "type": "string", + "default": "rgba(163, 21, 21, 1.00)" + }, + "isabelle.inner_quoted_dark_color": { + "type": "string", + "default": "rgba(206, 145, 120, 1.00)" + }, + "isabelle.inner_cartouche_light_color": { + "type": "string", + "default": "rgba(129, 31, 63, 1.00)" + }, + "isabelle.inner_cartouche_dark_color": { + "type": "string", + "default": "rgba(209, 105, 105, 1.00)" + }, + "isabelle.inner_comment_light_color": { + "type": "string", + "default": "rgba(0, 128, 0, 1.00)" + }, + "isabelle.inner_comment_dark_color": { + "type": "string", + "default": "rgba(96, 139, 78, 1.00)" + }, + "isabelle.dynamic_light_color": { + "type": "string", + "default": "rgba(121, 94, 38, 1.00)" + }, + "isabelle.dynamic_dark_color": { + "type": "string", + "default": "rgba(220, 220, 170, 1.00)" + }, + "isabelle.class_parameter_light_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.class_parameter_dark_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.antiquote_light_color": { + "type": "string", + "default": "rgba(102, 0, 204, 1.00)" + }, + "isabelle.antiquote_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + } } } },
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/content_provider.ts Sat Jun 17 14:52:23 2017 +0200 @@ -0,0 +1,35 @@ +'use strict' + +import { Event, EventEmitter, Uri, TextDocumentContentProvider, Disposable, + workspace } from 'vscode' + + +export class Content_Provider implements TextDocumentContentProvider +{ + private _uri_template: Uri + get uri_template(): Uri { return this._uri_template } + get uri_scheme(): string { return this.uri_template.scheme } + + constructor(uri_scheme: string) + { + this._uri_template = Uri.parse("scheme:").with({ scheme: uri_scheme }) + } + dispose() { } + + private emitter = new EventEmitter<Uri>() + public update(uri: Uri) { this.emitter.fire(uri) } + get onDidChange(): Event<Uri> { return this.emitter.event } + + private content = new Map<string, string>() + public set_content(uri: Uri, content: string) { this.content.set(uri.toString(), content)} + + provideTextDocumentContent(uri: Uri): string + { + return this.content.get(uri.toString()) || "" + } + + public register(): Disposable + { + return workspace.registerTextDocumentContentProvider(this.uri_scheme, this) + } +}
--- a/src/Tools/VSCode/extension/src/decorations.ts Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Jun 17 14:52:23 2017 +0200 @@ -65,11 +65,11 @@ ] -/* init */ +/* setup */ const types = new Map<string, TextEditorDecorationType>() -export function init(context: ExtensionContext) +export function setup(context: ExtensionContext) { function decoration(options: DecorationRenderOptions): TextEditorDecorationType {
--- a/src/Tools/VSCode/extension/src/extension.ts Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Sat Jun 17 14:52:23 2017 +0200 @@ -4,8 +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_panel from './state_panel'; import * as symbol from './symbol'; import * as completion from './completion'; import { ExtensionContext, workspace, window, commands, languages } from 'vscode'; @@ -48,9 +49,9 @@ /* decorations */ - decorations.init(context) + decorations.setup(context) context.subscriptions.push( - workspace.onDidChangeConfiguration(() => decorations.init(context)), + workspace.onDidChangeConfiguration(() => decorations.setup(context)), workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)), window.onDidChangeActiveTextEditor(decorations.update_editor), workspace.onDidCloseTextDocument(decorations.close_document)) @@ -101,15 +102,25 @@ }) - /* preview */ + /* state 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.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_panel.setup(context, language_client)) + - language_client.onReady().then(() => preview.init(context, language_client)) + /* preview panel */ + + context.subscriptions.push( + 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_panel.setup(context, language_client)) /* Isabelle symbols */ @@ -117,7 +128,7 @@ language_client.onReady().then(() => { language_client.onNotification(protocol.symbols_type, - params => symbol.init(context, params.entries)) + params => symbol.setup(context, params.entries)) language_client.sendNotification(protocol.symbols_request_type) })
--- a/src/Tools/VSCode/extension/src/preview.ts Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/src/preview.ts Sat Jun 17 14:52:23 2017 +0200 @@ -6,69 +6,45 @@ window, commands } from 'vscode' import { LanguageClient } from 'vscode-languageclient'; import * as library from './library' -import * as protocol from './protocol'; +import * as protocol from './protocol' +import { Content_Provider } from './content_provider' -/* Uri information */ +/* HTML content */ -const preview_uri_template = Uri.parse("isabelle-preview:") -const preview_uri_scheme = preview_uri_template.scheme +const content_provider = new Content_Provider("isabelle-preview") function encode_preview(document_uri: Uri | undefined): Uri | undefined { if (document_uri && library.is_file(document_uri)) { - return preview_uri_template.with({ query: document_uri.fsPath }) + return content_provider.uri_template.with({ query: document_uri.fsPath }) } else undefined } function decode_preview(preview_uri: Uri | undefined): Uri | undefined { - if (preview_uri && preview_uri.scheme === preview_uri_scheme) { + if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) { return Uri.file(preview_uri.query) } else undefined } -/* HTML content */ - -const preview_content = new Map<string, string>() - -class Content_Provider implements TextDocumentContentProvider -{ - dispose() { } - - private emitter = new EventEmitter<Uri>() - public update(preview_uri: Uri) { this.emitter.fire(preview_uri) } - get onDidChange(): Event<Uri> { return this.emitter.event } - - provideTextDocumentContent(preview_uri: Uri): string - { - return preview_content.get(preview_uri.toString()) || "" - } -} - - -/* init */ +/* setup */ let language_client: LanguageClient -let content_provider: Content_Provider - -export function init(context: ExtensionContext, client: LanguageClient) -{ - language_client = client - content_provider = new Content_Provider() - context.subscriptions.push( - workspace.registerTextDocumentContentProvider(preview_uri_scheme, content_provider), - content_provider) +export function setup(context: ExtensionContext, client: LanguageClient) +{ + context.subscriptions.push(content_provider.register()) + language_client = client language_client.onNotification(protocol.preview_response_type, params => { const preview_uri = encode_preview(Uri.parse(params.uri)) if (preview_uri) { - preview_content.set(preview_uri.toString(), params.content) + content_provider.set_content(preview_uri, params.content) content_provider.update(preview_uri) const existing_document =
--- a/src/Tools/VSCode/extension/src/protocol.ts Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/src/protocol.ts Sat Jun 17 14:52:23 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/extension/src/symbol.ts Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/extension/src/symbol.ts Sat Jun 17 14:52:23 2017 +0200 @@ -113,7 +113,7 @@ registerSubstitutions: (substitutions: LanguageEntry) => Disposable } -export function init(context: ExtensionContext, entries: [Entry]) +export function setup(context: ExtensionContext, entries: [Entry]) { update_entries(entries)
--- a/src/Tools/VSCode/src/document_model.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sat Jun 17 14:52:23 2017 +0200 @@ -48,12 +48,13 @@ catch { case ERROR(_) => Nil } } - def init(session: Session, node_name: Document.Node.Name): Document_Model = - Document_Model(session, node_name, Content.empty) + def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = + Document_Model(session, editor, node_name, Content.empty) } sealed case class Document_Model( session: Session, + editor: Server.Editor, node_name: Document.Node.Name, content: Document_Model.Content, external_file: Boolean = false, @@ -109,8 +110,10 @@ case None => Text.Perspective.empty } + val overlays = editor.node_overlays(node_name) + (snapshot.node.load_commands_changed(doc_blobs), - Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)) + Document.Node.Perspective(node_required, text_perspective, overlays)) } else (false, Document.Node.no_perspective_text) }
--- a/src/Tools/VSCode/src/preview.scala Thu Jun 15 17:22:23 2017 +0100 +++ /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 Sat Jun 17 14:52:23 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/protocol.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Sat Jun 17 14:52:23 2017 +0200 @@ -462,10 +462,33 @@ object Dynamic_Output { - def apply(body: String): JSON.T = - Notification("PIDE/dynamic_output", Map("content" -> body)) + def apply(content: String): JSON.T = + Notification("PIDE/dynamic_output", Map("content" -> content)) + } + + + /* 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 */
--- a/src/Tools/VSCode/src/server.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Jun 17 14:52:23 2017 +0200 @@ -21,6 +21,9 @@ object Server { + type Editor = isabelle.Editor[Unit] + + /* Isabelle tool wrapper */ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") @@ -118,7 +121,8 @@ private val delay_load: Standard_Thread.Delay = Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) { - val (invoke_input, invoke_load) = resources.resolve_dependencies(session, file_watcher) + val (invoke_input, invoke_load) = + resources.resolve_dependencies(session, editor, file_watcher) if (invoke_input) delay_input.invoke() if (invoke_load) delay_load.invoke } @@ -158,7 +162,7 @@ } norm(changes) norm_changes.foreach(change => - resources.change_model(session, file, change.text, change.range)) + resources.change_model(session, editor, file, change.text, change.range)) delay_input.invoke() delay_output.invoke() @@ -181,17 +185,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,6 +404,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_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") @@ -426,12 +434,17 @@ /* abstract editor operations */ - object editor extends Editor[Unit] + object editor extends Server.Editor { + /* session */ + override def session: Session = server.session override def flush(): Unit = resources.flush_input(session) override def invoke(): Unit = delay_input.invoke() + + /* current situation */ + override def current_node(context: Unit): Option[Document.Node.Name] = resources.get_caret().map(_.model.node_name) override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = @@ -455,8 +468,31 @@ override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = current_command(snapshot) + + /* overlays */ + + override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + resources.node_overlays(name) + + override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + resources.insert_overlay(command, fn, args) + + override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + resources.remove_overlay(command, fn, args) + + + /* hyperlinks */ + override def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) : Option[Hyperlink] = None + + + /* dispatcher thread */ + + override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) + override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) + override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) + override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) } }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/state_panel.scala Sat Jun 17 14:52:23 2017 +0200 @@ -0,0 +1,121 @@ +/* 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() { 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 + } +}
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Jun 17 14:52:23 2017 +0200 @@ -21,6 +21,7 @@ sealed case class State( models: Map[JFile, Document_Model] = Map.empty, caret: Option[(JFile, Line.Position)] = None, + overlays: Document.Overlays = Document.Overlays.empty, pending_input: Set[JFile] = Set.empty, pending_output: Set[JFile] = Set.empty) { @@ -49,6 +50,14 @@ (_, model) <- models.iterator blob <- model.get_blob } yield (model.node_name -> blob)).toMap) + + def change_overlay(insert: Boolean, file: JFile, + command: Command, fn: String, args: List[String]): State = + copy( + overlays = + if (insert) overlays.insert(command, fn, args) + else overlays.remove(command, fn, args), + pending_input = pending_input + file) } @@ -147,11 +156,16 @@ case None => false } - def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None) + def change_model( + session: Session, + editor: Server.Editor, + file: JFile, + text: String, + range: Option[Line.Range] = None) { state.change(st => { - val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file))) + val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) val model1 = (model.change_text(text, range) getOrElse model).external(false) st.update_models(Some(file -> model1)) }) @@ -178,9 +192,24 @@ }) + /* overlays */ + + def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + state.value.overlays(name) + + def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) + + def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) + + /* resolve dependencies */ - def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) = + def resolve_dependencies( + session: Session, + editor: Server.Editor, + file_watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => { @@ -217,7 +246,7 @@ text <- { file_watcher.register_parent(file); read_file_content(file) } } yield { - val model = Document_Model.init(session, node_name) + val model = Document_Model.init(session, editor, node_name) val model1 = (model.change_text(text) getOrElse model).external(true) (file, model1) }).toList
--- a/src/Tools/jEdit/src/document_model.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sat Jun 17 14:52:23 2017 +0200 @@ -27,7 +27,8 @@ sealed case class State( models: Map[Document.Node.Name, Document_Model] = Map.empty, - buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty) + buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty, + overlays: Document.Overlays = Document.Overlays.empty) { def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = for { @@ -83,6 +84,18 @@ } yield info.map((_, model)) + /* overlays */ + + def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + state.value.overlays(name) + + def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args))) + + def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args))) + + /* sync external files */ def sync_files(changed_files: Set[JFile]): Boolean =
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Jun 17 14:52:23 2017 +0200 @@ -83,6 +83,18 @@ } + /* overlays */ + + override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + Document_Model.node_overlays(name) + + override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + Document_Model.insert_overlay(command, fn, args) + + override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + Document_Model.remove_overlay(command, fn, args) + + /* navigation */ def push_position(view: View) @@ -284,4 +296,12 @@ hyperlink_command(focus, snapshot, id, range.start) case _ => None } + + + /* dispatcher thread */ + + override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body) + override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body) + override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body) + override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body) }
--- a/src/Tools/jEdit/src/state_dockable.scala Thu Jun 15 17:22:23 2017 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Sat Jun 17 14:52:23 2017 +0200 @@ -64,7 +64,7 @@ { GUI_Thread.require {} - Document_Model.get(view.getBuffer).map(_.snapshot()) match { + PIDE.editor.current_node_snapshot(view) match { case Some(snapshot) => (PIDE.editor.current_command(view, snapshot), print_state.get_location) match { case (Some(command1), Some(command2)) if command1.id == command2.id =>