# HG changeset patch
# User wenzelm
# Date 1375868657 -7200
# Node ID 98eac7b7eec3d996d635c1129654f448ad3e6b2f
# Parent  1e22e8101f4714272accc60b4ac9907007540cf4
tuned signature;

diff -r 1e22e8101f47 -r 98eac7b7eec3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 07 11:44:17 2013 +0200
@@ -15,48 +15,6 @@
 {
   /** document structure **/
 
-  /* overlays -- print functions with arguments */
-
-  type Overlay = (Command, (String, List[String]))
-
-  object Overlays
-  {
-    val empty = new Overlays(Map.empty)
-  }
-
-  final class Overlays private(rep: Map[Command, List[(String, List[String])]])
-  {
-    def commands: Set[Command] = rep.keySet
-    def is_empty: Boolean = rep.isEmpty
-
-    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
-  }
-
-
   /* individual nodes */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
@@ -65,6 +23,11 @@
 
   object Node
   {
+    val empty: Node = new Node()
+
+
+    /* header and name */
+
     sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
@@ -84,6 +47,7 @@
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
     }
+
     sealed case class Name(node: String, dir: String, theory: String)
     {
       override def hashCode: Int = node.hashCode
@@ -95,6 +59,51 @@
       override def toString: String = theory
     }
 
+
+    /* overlays -- print functions with arguments */
+
+    type Overlay = (Command, (String, List[String]))
+
+    object Overlays
+    {
+      val empty = new Overlays(Map.empty)
+    }
+
+    final class Overlays private(rep: Map[Command, List[(String, List[String])]])
+    {
+      def commands: Set[Command] = rep.keySet
+      def is_empty: Boolean = rep.isEmpty
+
+      def insert(cmd: Command, over: (String, List[String])): Overlays =
+      {
+        val overs = rep.getOrElse(cmd, Nil)
+        if (overs.contains(over)) this
+        else new Overlays(rep + (cmd -> (over :: overs)))
+      }
+
+      def remove(cmd: Command, over: (String, List[String])): Overlays =
+        rep.get(cmd) match {
+          case Some(overs) =>
+            if (overs.contains(over)) {
+              overs.filterNot(_ == over) match {
+                case Nil => new Overlays(rep - cmd)
+                case overs1 => new Overlays(rep + (cmd -> overs1))
+              }
+            }
+            else this
+          case None => this
+        }
+
+      def dest: List[Overlay] =
+        (for {
+          (cmd, overs) <- rep.iterator
+          over <- overs
+        } yield (cmd, over)).toList
+    }
+
+
+    /* edits */
+
     sealed abstract class Edit[A, B]
     {
       def foreach(f: A => Unit)
@@ -112,6 +121,9 @@
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
+
+    /* commands */
+
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -124,14 +136,12 @@
     }
 
     private val block_size = 1024
-
-    val empty: Node = new Node()
   }
 
   final class Node private(
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Node.Perspective_Command =
-      Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
+      Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
diff -r 1e22e8101f47 -r 98eac7b7eec3 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 11:44:17 2013 +0200
@@ -95,7 +95,7 @@
   def command_perspective(
       node: Document.Node,
       perspective: Text.Perspective,
-      overlays: Document.Overlays): (Command.Perspective, Command.Perspective) =
+      overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
   {
     if (perspective.is_empty && overlays.is_empty)
       (Command.Perspective.empty, Command.Perspective.empty)
diff -r 1e22e8101f47 -r 98eac7b7eec3 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 07 11:44:17 2013 +0200
@@ -79,7 +79,7 @@
 
   /* overlays */
 
-  private var overlays = Document.Overlays.empty
+  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)) }
@@ -104,7 +104,7 @@
   }
 
   val empty_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
 
   def node_perspective(): Document.Node.Perspective_Text =
   {