# HG changeset patch # User wenzelm # Date 1375709350 -7200 # Node ID 930ce8eacb87b319e6c2aece86f2e8503b2c81b2 # Parent e93d73b51fd0030d50a16bce9d26abffe495c8b7 tuned signature -- more uniform treatment of overlays as command mapping; diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Pure/PIDE/document.ML Mon Aug 05 15:29:10 2013 +0200 @@ -9,7 +9,7 @@ sig val timing: bool Unsynchronized.ref type node_header = string * Thy_Header.header * string list - type overlay = Document_ID.command * string * string list + type overlay = Document_ID.command * (string * string list) datatype node_edit = Clear | (* FIXME unused !? *) Edits of (Document_ID.command option * Document_ID.command option) list | @@ -68,7 +68,7 @@ {required = required, visible = Inttab.make_set command_ids, visible_last = try List.last command_ids, - overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)}; + overlays = Inttab.make_list overlays}; val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]); val no_perspective = make_perspective (false, [], []); @@ -135,7 +135,7 @@ (* node edits and associated executions *) -type overlay = Document_ID.command * string * string list; +type overlay = Document_ID.command * (string * string list); datatype node_edit = Clear | diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Pure/PIDE/document.scala Mon Aug 05 15:29:10 2013 +0200 @@ -17,20 +17,43 @@ /* overlays -- print functions with arguments */ - type Overlay = (Command, String, List[String]) + type Overlay = (Command, (String, List[String])) object Overlays { - val empty = new Overlays(Set.empty) + val empty = new Overlays(Map.empty) } - final class Overlays private(rep: Set[Overlay]) + final class Overlays private(rep: Map[Command, List[(String, List[String])]]) { - def + (o: Overlay) = new Overlays(rep + o) - def - (o: Overlay) = new Overlays(rep - o) + def commands: Set[Command] = rep.keySet def is_empty: Boolean = rep.isEmpty - def dest: List[Overlay] = rep.toList - def commands: Set[Command] = rep.iterator.map(x => x._1).toSet + + def insert(cmd: Command, fn: (String, List[String])): Overlays = + { + val fns = rep.get(cmd) getOrElse Nil + if (fns.contains(fn)) this + else new Overlays(rep + (cmd -> (fn :: fns))) + } + + def remove(cmd: Command, fn: (String, List[String])): Overlays = + rep.get(cmd) match { + case Some(fns) => + if (fns.contains(fn)) { + fns.filterNot(_ == fn) match { + case Nil => new Overlays(rep - cmd) + case fns1 => new Overlays(rep + (cmd -> fns1)) + } + } + else this + case None => this + } + + def dest: List[Overlay] = + (for { + (cmd, fns) <- rep.iterator + fn <- fns + } yield (cmd, fn)).toList } diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Mon Aug 05 15:29:10 2013 +0200 @@ -58,7 +58,7 @@ in Document.Deps (master, header, errors) end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, - list (triple int string (list string)) c)])) + list (pair int (pair string (list string))) c)])) end; val (removed, assign_update, state') = Document.update old_id new_id edits state; diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Pure/PIDE/protocol.scala Mon Aug 05 15:29:10 2013 +0200 @@ -342,7 +342,7 @@ (dir, (name.theory, (imports, (keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), - list(triple(id, Encode.string, list(Encode.string)))(c.dest)) })) + list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { val (name, edit) = node_edit diff -r e93d73b51fd0 -r 930ce8eacb87 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 05 15:29:10 2013 +0200 @@ -81,11 +81,11 @@ private var overlays = Document.Overlays.empty - def add_overlay(command: Command, name: String, args: List[String]): Unit = - Swing_Thread.require { overlays += ((command, name, args)) } + 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 -= ((command, name, args)) } + Swing_Thread.require { overlays = overlays.remove(command, (name, args)) } /* perspective */ diff -r e93d73b51fd0 -r 930ce8eacb87 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Mon Aug 05 15:03:52 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Mon Aug 05 15:29:10 2013 +0200 @@ -114,7 +114,7 @@ case Some(command) => current_location = Some(command) current_query = query - doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query)) + doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query)) case None => } case None =>