src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -23,15 +23,6 @@
   val NO_ID = ""
 
 
-  /* nodes */
-
-  object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) }  // FIXME None: remove
-
-  type Edit[C] =
-   (String,  // node name
-    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
-
-
   /* command start positions */
 
   def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
@@ -45,21 +36,65 @@
   }
 
 
+  /* named document nodes */
+
+  object Node
+  {
+    val empty: Node = new Node(Linear_Set())
+  }
+
+  class Node(val commands: Linear_Set[Command])
+  {
+    /* command ranges */
+
+    def command_starts: Iterator[(Command, Int)] =
+      Document.command_starts(commands.iterator)
+
+    def command_start(cmd: Command): Option[Int] =
+      command_starts.find(_._1 == cmd).map(_._2)
+
+    def command_range(i: Int): Iterator[(Command, Int)] =
+      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+
+    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+      command_range(i) takeWhile { case (_, start) => start < j }
+
+    def command_at(i: Int): Option[(Command, Int)] =
+    {
+      val range = command_range(i)
+      if (range.hasNext) Some(range.next) else None
+    }
+
+    def proper_command_at(i: Int): Option[Command] =
+      command_at(i) match {
+        case Some((command, _)) =>
+          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+        case None => None
+      }
+  }
+
+
   /* initial document */
 
   val init: Document =
   {
-    val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
+    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
     doc.assign_states(Nil)
     doc
   }
 
 
 
-  /** document edits **/
+  /** editing **/
+
+  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
+
+  type Edit[C] =
+   (String,  // node name
+    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
   def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
-      edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
+      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   {
     require(old_doc.assignment.is_finished)
 
@@ -145,7 +180,7 @@
       var former_states = old_doc.assignment.join
 
       for ((name, text_edits) <- edits) {
-        val commands0 = nodes(name)
+        val commands0 = nodes(name).commands
         val commands1 = edit_text(text_edits, commands0)
         val commands2 = parse_spans(commands1)
 
@@ -157,7 +192,7 @@
           inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
         doc_edits += (name -> Some(cmd_edits))
-        nodes += (name -> commands2)
+        nodes += (name -> new Node(commands2))
         former_states --= removed_commands
       }
       (doc_edits.toList, new Document(new_id, nodes, former_states))
@@ -168,39 +203,9 @@
 
 class Document(
     val id: Document.Version_ID,
-    val nodes: Map[String, Linear_Set[Command]],
+    val nodes: Map[String, Document.Node],
     former_states: Map[Command, Command])  // FIXME !?
 {
-  /* command ranges */
-
-  def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
-
-  def command_starts(name: String): Iterator[(Command, Int)] =
-    Document.command_starts(commands(name).iterator)
-
-  def command_start(name: String, cmd: Command): Option[Int] =
-    command_starts(name).find(_._1 == cmd).map(_._2)
-
-  def command_range(name: String, i: Int): Iterator[(Command, Int)] =
-    command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
-
-  def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
-    command_range(name, i) takeWhile { case (_, start) => start < j }
-
-  def command_at(name: String, i: Int): Option[(Command, Int)] =
-  {
-    val range = command_range(name, i)
-    if (range.hasNext) Some(range.next) else None
-  }
-
-  def proper_command_at(name: String, i: Int): Option[Command] =
-    command_at(name, i) match {
-      case Some((command, _)) =>
-        commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
-      case None => None
-    }
-
-
   /* command state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]