tuned signature -- more uniform treatment of overlays as command mapping;
authorwenzelm
Mon Aug 05 15:29:10 2013 +0200 (2013-08-05)
changeset 52862930ce8eacb87
parent 52861 e93d73b51fd0
child 52863 acbced24e5fc
tuned signature -- more uniform treatment of overlays as command mapping;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 05 15:03:52 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 05 15:29:10 2013 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val timing: bool Unsynchronized.ref
     1.6    type node_header = string * Thy_Header.header * string list
     1.7 -  type overlay = Document_ID.command * string * string list
     1.8 +  type overlay = Document_ID.command * (string * string list)
     1.9    datatype node_edit =
    1.10      Clear |    (* FIXME unused !? *)
    1.11      Edits of (Document_ID.command option * Document_ID.command option) list |
    1.12 @@ -68,7 +68,7 @@
    1.13   {required = required,
    1.14    visible = Inttab.make_set command_ids,
    1.15    visible_last = try List.last command_ids,
    1.16 -  overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
    1.17 +  overlays = Inttab.make_list overlays};
    1.18  
    1.19  val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
    1.20  val no_perspective = make_perspective (false, [], []);
    1.21 @@ -135,7 +135,7 @@
    1.22  
    1.23  (* node edits and associated executions *)
    1.24  
    1.25 -type overlay = Document_ID.command * string * string list;
    1.26 +type overlay = Document_ID.command * (string * string list);
    1.27  
    1.28  datatype node_edit =
    1.29    Clear |
     2.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 05 15:03:52 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon Aug 05 15:29:10 2013 +0200
     2.3 @@ -17,20 +17,43 @@
     2.4  
     2.5    /* overlays -- print functions with arguments */
     2.6  
     2.7 -  type Overlay = (Command, String, List[String])
     2.8 +  type Overlay = (Command, (String, List[String]))
     2.9  
    2.10    object Overlays
    2.11    {
    2.12 -    val empty = new Overlays(Set.empty)
    2.13 +    val empty = new Overlays(Map.empty)
    2.14    }
    2.15  
    2.16 -  final class Overlays private(rep: Set[Overlay])
    2.17 +  final class Overlays private(rep: Map[Command, List[(String, List[String])]])
    2.18    {
    2.19 -    def + (o: Overlay) = new Overlays(rep + o)
    2.20 -    def - (o: Overlay) = new Overlays(rep - o)
    2.21 +    def commands: Set[Command] = rep.keySet
    2.22      def is_empty: Boolean = rep.isEmpty
    2.23 -    def dest: List[Overlay] = rep.toList
    2.24 -    def commands: Set[Command] = rep.iterator.map(x => x._1).toSet
    2.25 +
    2.26 +    def insert(cmd: Command, fn: (String, List[String])): Overlays =
    2.27 +    {
    2.28 +      val fns = rep.get(cmd) getOrElse Nil
    2.29 +      if (fns.contains(fn)) this
    2.30 +      else new Overlays(rep + (cmd -> (fn :: fns)))
    2.31 +    }
    2.32 +
    2.33 +    def remove(cmd: Command, fn: (String, List[String])): Overlays =
    2.34 +      rep.get(cmd) match {
    2.35 +        case Some(fns) =>
    2.36 +          if (fns.contains(fn)) {
    2.37 +            fns.filterNot(_ == fn) match {
    2.38 +              case Nil => new Overlays(rep - cmd)
    2.39 +              case fns1 => new Overlays(rep + (cmd -> fns1))
    2.40 +            }
    2.41 +          }
    2.42 +          else this
    2.43 +        case None => this
    2.44 +      }
    2.45 +
    2.46 +    def dest: List[Overlay] =
    2.47 +      (for {
    2.48 +        (cmd, fns) <- rep.iterator
    2.49 +        fn <- fns
    2.50 +      } yield (cmd, fn)).toList
    2.51    }
    2.52  
    2.53  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:03:52 2013 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:29:10 2013 +0200
     3.3 @@ -58,7 +58,7 @@
     3.4                      in Document.Deps (master, header, errors) end,
     3.5                    fn (a :: b, c) =>
     3.6                      Document.Perspective (bool_atom a, map int_atom b,
     3.7 -                      list (triple int string (list string)) c)]))
     3.8 +                      list (pair int (pair string (list string))) c)]))
     3.9              end;
    3.10  
    3.11          val (removed, assign_update, state') = Document.update old_id new_id edits state;
     4.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:03:52 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:29:10 2013 +0200
     4.3 @@ -342,7 +342,7 @@
     4.4                  (dir, (name.theory, (imports, (keywords, header.errors)))))) },
     4.5            { case Document.Node.Perspective(a, b, c) =>
     4.6                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
     4.7 -                list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
     4.8 +                list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
     4.9        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    4.10        {
    4.11          val (name, edit) = node_edit
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 05 15:03:52 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 05 15:29:10 2013 +0200
     5.3 @@ -81,11 +81,11 @@
     5.4  
     5.5    private var overlays = Document.Overlays.empty
     5.6  
     5.7 -  def add_overlay(command: Command, name: String, args: List[String]): Unit =
     5.8 -    Swing_Thread.require { overlays += ((command, name, args)) }
     5.9 +  def insert_overlay(command: Command, name: String, args: List[String]): Unit =
    5.10 +    Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
    5.11  
    5.12    def remove_overlay(command: Command, name: String, args: List[String]): Unit =
    5.13 -    Swing_Thread.require { overlays -= ((command, name, args)) }
    5.14 +    Swing_Thread.require { overlays = overlays.remove(command, (name, args)) }
    5.15  
    5.16  
    5.17    /* perspective */
     6.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:03:52 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:29:10 2013 +0200
     6.3 @@ -114,7 +114,7 @@
     6.4            case Some(command) =>
     6.5              current_location = Some(command)
     6.6              current_query = query
     6.7 -            doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
     6.8 +            doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query))
     6.9            case None =>
    6.10          }
    6.11        case None =>