# HG changeset patch # User wenzelm # Date 1376310478 -7200 # Node ID 15254e32d2996df07661c7e67dd2a08af3afd703 # Parent c3d82d58beaff880369365fc9a37b79380cce0fe central management of Document.Overlays, independent of Document_Model; diff -r c3d82d58beaf -r 15254e32d299 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Aug 12 13:32:26 2013 +0200 +++ b/src/Pure/PIDE/document.scala Mon Aug 12 14:27:58 2013 +0200 @@ -15,6 +15,32 @@ { /** document structure **/ + /* overlays -- print functions with arguments */ + + object Overlays + { + val empty = new Overlays(Map.empty) + } + + final class Overlays private(rep: Map[Node.Name, Node.Overlays]) + { + def apply(name: Document.Node.Name): Node.Overlays = + rep.getOrElse(name, Node.Overlays.empty) + + private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = + { + val node_overlays = f(apply(name)) + new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays)) + } + + def insert(command: Command, fn: String, args: List[String]): Overlays = + update(command.node_name, _.insert(command, fn, args)) + + def remove(command: Command, fn: String, args: List[String]): Overlays = + update(command.node_name, _.remove(command, fn, args)) + } + + /* individual nodes */ type Edit[A, B] = (Node.Name, Node.Edit[A, B]) @@ -60,27 +86,22 @@ } - /* overlays -- print functions with arguments */ - - type Print_Function = (String, List[String]) + /* node overlays */ object Overlays { val empty = new Overlays(Multi_Map.empty) } - final class Overlays private(rep: Multi_Map[Command, Print_Function]) + final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) { def commands: Set[Command] = rep.keySet def is_empty: Boolean = rep.isEmpty - - def insert(cmd: Command, over: Print_Function): Overlays = - new Overlays(rep.insert(cmd, over)) - - def remove(cmd: Command, over: Print_Function): Overlays = - new Overlays(rep.remove(cmd, over)) - - def dest: List[(Command, Print_Function)] = rep.iterator.toList + def dest: List[(Command, (String, List[String]))] = rep.iterator.toList + def insert(cmd: Command, fn: String, args: List[String]): Overlays = + new Overlays(rep.insert(cmd, (fn, args))) + def remove(cmd: Command, fn: String, args: List[String]): Overlays = + new Overlays(rep.remove(cmd, (fn, args))) } diff -r c3d82d58beaf -r 15254e32d299 src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Mon Aug 12 13:32:26 2013 +0200 +++ b/src/Pure/PIDE/editor.scala Mon Aug 12 14:27:58 2013 +0200 @@ -16,5 +16,9 @@ def current_snapshot(context: Context): Option[Document.Snapshot] def node_snapshot(name: Document.Node.Name): Document.Snapshot def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] + + def node_overlays(name: Document.Node.Name): Document.Node.Overlays + def insert_overlay(command: Command, fn: String, args: List[String]): Unit + def remove_overlay(command: Command, fn: String, args: List[String]): Unit } diff -r c3d82d58beaf -r 15254e32d299 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Aug 12 13:32:26 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 12 14:27:58 2013 +0200 @@ -77,17 +77,6 @@ } - /* overlays */ - - private var overlays = Document.Node.Overlays.empty - - def insert_overlay(command: Command, name: String, args: List[String]): Unit = - Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } - - def remove_overlay(command: Command, name: String, args: List[String]): Unit = - Swing_Thread.require { overlays = overlays.remove(command, (name, args)) } - - /* perspective */ // owned by Swing thread @@ -115,7 +104,7 @@ for { doc_view <- PIDE.document_views(buffer) range <- doc_view.perspective().ranges - } yield range), overlays) + } yield range), PIDE.editor.node_overlays(node_name)) } else empty_perspective } diff -r c3d82d58beaf -r 15254e32d299 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 13:32:26 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 14:27:58 2013 +0200 @@ -15,6 +15,8 @@ class JEdit_Editor extends Editor[View] { + /* session */ + def session: Session = PIDE.session def flush() @@ -34,6 +36,9 @@ ) } + + /* current situation */ + def current_context: View = Swing_Thread.require { jEdit.getActiveView() } @@ -72,4 +77,18 @@ } } } + + + /* overlays */ + + private var overlays = Document.Overlays.empty + + def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + synchronized { overlays(name) } + + def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + synchronized { overlays = overlays.insert(command, fn, args) } + + def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + synchronized { overlays = overlays.remove(command, fn, args) } } diff -r c3d82d58beaf -r 15254e32d299 src/Tools/jEdit/src/query_operation.scala --- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 13:32:26 2013 +0200 +++ b/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 14:27:58 2013 +0200 @@ -56,13 +56,8 @@ private def remove_overlay() { - Swing_Thread.require() - - for { - command <- current_location - buffer <- JEdit_Lib.jedit_buffer(command.node_name.node) - model <- PIDE.document_model(buffer) - } model.remove_overlay(command, operation_name, instance :: current_query) + current_location.foreach(command => + editor.remove_overlay(command, operation_name, instance :: current_query)) } @@ -167,7 +162,7 @@ current_location = Some(command) current_query = query current_status = Query_Operation.Status.WAITING - doc_view.model.insert_overlay(command, operation_name, instance :: query) + editor.insert_overlay(command, operation_name, instance :: query) case None => } consume_status(current_status)