# HG changeset patch # User wenzelm # Date 1497703656 -7200 # Node ID 0f0f294e314f6f86120d8de1c9a50e133a005e34 # Parent d1ad5a7458c26443661137099e0c7c227cd5b4b6 maintain overlays within main state of document models; proper pending_input for Isabelle/VSCode; diff -r d1ad5a7458c2 -r 0f0f294e314f src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Fri Jun 16 22:40:05 2017 +0200 +++ b/src/Pure/PIDE/editor.scala Sat Jun 17 14:47:36 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 */ diff -r d1ad5a7458c2 -r 0f0f294e314f src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Fri Jun 16 22:40:05 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Sat Jun 17 14:47:36 2017 +0200 @@ -436,10 +436,15 @@ 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] = @@ -463,10 +468,28 @@ 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) diff -r d1ad5a7458c2 -r 0f0f294e314f src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Fri Jun 16 22:40:05 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Jun 17 14:47:36 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) } @@ -183,6 +192,18 @@ }) + /* 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( diff -r d1ad5a7458c2 -r 0f0f294e314f src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Jun 16 22:40:05 2017 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Jun 17 14:47:36 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 = diff -r d1ad5a7458c2 -r 0f0f294e314f src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Fri Jun 16 22:40:05 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Jun 17 14:47:36 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)