central management of Document.Overlays, independent of Document_Model;
authorwenzelm
Mon Aug 12 14:27:58 2013 +0200 (2013-08-12)
changeset 5297715254e32d299
parent 52976 c3d82d58beaf
child 52978 37fbb3fde380
central management of Document.Overlays, independent of Document_Model;
src/Pure/PIDE/document.scala
src/Pure/PIDE/editor.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/query_operation.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 12 13:32:26 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Aug 12 14:27:58 2013 +0200
     1.3 @@ -15,6 +15,32 @@
     1.4  {
     1.5    /** document structure **/
     1.6  
     1.7 +  /* overlays -- print functions with arguments */
     1.8 +
     1.9 +  object Overlays
    1.10 +  {
    1.11 +    val empty = new Overlays(Map.empty)
    1.12 +  }
    1.13 +
    1.14 +  final class Overlays private(rep: Map[Node.Name, Node.Overlays])
    1.15 +  {
    1.16 +    def apply(name: Document.Node.Name): Node.Overlays =
    1.17 +      rep.getOrElse(name, Node.Overlays.empty)
    1.18 +
    1.19 +    private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
    1.20 +    {
    1.21 +      val node_overlays = f(apply(name))
    1.22 +      new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
    1.23 +    }
    1.24 +
    1.25 +    def insert(command: Command, fn: String, args: List[String]): Overlays =
    1.26 +      update(command.node_name, _.insert(command, fn, args))
    1.27 +
    1.28 +    def remove(command: Command, fn: String, args: List[String]): Overlays =
    1.29 +      update(command.node_name, _.remove(command, fn, args))
    1.30 +  }
    1.31 +
    1.32 +
    1.33    /* individual nodes */
    1.34  
    1.35    type Edit[A, B] = (Node.Name, Node.Edit[A, B])
    1.36 @@ -60,27 +86,22 @@
    1.37      }
    1.38  
    1.39  
    1.40 -    /* overlays -- print functions with arguments */
    1.41 -
    1.42 -    type Print_Function = (String, List[String])
    1.43 +    /* node overlays */
    1.44  
    1.45      object Overlays
    1.46      {
    1.47        val empty = new Overlays(Multi_Map.empty)
    1.48      }
    1.49  
    1.50 -    final class Overlays private(rep: Multi_Map[Command, Print_Function])
    1.51 +    final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
    1.52      {
    1.53        def commands: Set[Command] = rep.keySet
    1.54        def is_empty: Boolean = rep.isEmpty
    1.55 -
    1.56 -      def insert(cmd: Command, over: Print_Function): Overlays =
    1.57 -        new Overlays(rep.insert(cmd, over))
    1.58 -
    1.59 -      def remove(cmd: Command, over: Print_Function): Overlays =
    1.60 -        new Overlays(rep.remove(cmd, over))
    1.61 -
    1.62 -      def dest: List[(Command, Print_Function)] = rep.iterator.toList
    1.63 +      def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
    1.64 +      def insert(cmd: Command, fn: String, args: List[String]): Overlays =
    1.65 +        new Overlays(rep.insert(cmd, (fn, args)))
    1.66 +      def remove(cmd: Command, fn: String, args: List[String]): Overlays =
    1.67 +        new Overlays(rep.remove(cmd, (fn, args)))
    1.68      }
    1.69  
    1.70  
     2.1 --- a/src/Pure/PIDE/editor.scala	Mon Aug 12 13:32:26 2013 +0200
     2.2 +++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 14:27:58 2013 +0200
     2.3 @@ -16,5 +16,9 @@
     2.4    def current_snapshot(context: Context): Option[Document.Snapshot]
     2.5    def node_snapshot(name: Document.Node.Name): Document.Snapshot
     2.6    def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
     2.7 +
     2.8 +  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
     2.9 +  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
    2.10 +  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
    2.11  }
    2.12  
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 13:32:26 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 14:27:58 2013 +0200
     3.3 @@ -77,17 +77,6 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* overlays */
     3.8 -
     3.9 -  private var overlays = Document.Node.Overlays.empty
    3.10 -
    3.11 -  def insert_overlay(command: Command, name: String, args: List[String]): Unit =
    3.12 -    Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
    3.13 -
    3.14 -  def remove_overlay(command: Command, name: String, args: List[String]): Unit =
    3.15 -    Swing_Thread.require { overlays = overlays.remove(command, (name, args)) }
    3.16 -
    3.17 -
    3.18    /* perspective */
    3.19  
    3.20    // owned by Swing thread
    3.21 @@ -115,7 +104,7 @@
    3.22          for {
    3.23            doc_view <- PIDE.document_views(buffer)
    3.24            range <- doc_view.perspective().ranges
    3.25 -        } yield range), overlays)
    3.26 +        } yield range), PIDE.editor.node_overlays(node_name))
    3.27      }
    3.28      else empty_perspective
    3.29    }
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 13:32:26 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
     4.3 @@ -15,6 +15,8 @@
     4.4  
     4.5  class JEdit_Editor extends Editor[View]
     4.6  {
     4.7 +  /* session */
     4.8 +
     4.9    def session: Session = PIDE.session
    4.10  
    4.11    def flush()
    4.12 @@ -34,6 +36,9 @@
    4.13      )
    4.14    }
    4.15  
    4.16 +
    4.17 +  /* current situation */
    4.18 +
    4.19    def current_context: View =
    4.20      Swing_Thread.require { jEdit.getActiveView() }
    4.21  
    4.22 @@ -72,4 +77,18 @@
    4.23        }
    4.24      }
    4.25    }
    4.26 +
    4.27 +
    4.28 +  /* overlays */
    4.29 +
    4.30 +  private var overlays = Document.Overlays.empty
    4.31 +
    4.32 +  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    4.33 +    synchronized { overlays(name) }
    4.34 +
    4.35 +  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    4.36 +    synchronized { overlays = overlays.insert(command, fn, args) }
    4.37 +
    4.38 +  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    4.39 +    synchronized { overlays = overlays.remove(command, fn, args) }
    4.40  }
     5.1 --- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 13:32:26 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 14:27:58 2013 +0200
     5.3 @@ -56,13 +56,8 @@
     5.4  
     5.5    private def remove_overlay()
     5.6    {
     5.7 -    Swing_Thread.require()
     5.8 -
     5.9 -    for {
    5.10 -      command <- current_location
    5.11 -      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    5.12 -      model <- PIDE.document_model(buffer)
    5.13 -    } model.remove_overlay(command, operation_name, instance :: current_query)
    5.14 +    current_location.foreach(command =>
    5.15 +      editor.remove_overlay(command, operation_name, instance :: current_query))
    5.16    }
    5.17  
    5.18  
    5.19 @@ -167,7 +162,7 @@
    5.20              current_location = Some(command)
    5.21              current_query = query
    5.22              current_status = Query_Operation.Status.WAITING
    5.23 -            doc_view.model.insert_overlay(command, operation_name, instance :: query)
    5.24 +            editor.insert_overlay(command, operation_name, instance :: query)
    5.25            case None =>
    5.26          }
    5.27          consume_status(current_status)