# HG changeset patch
# User wenzelm
# Date 1330272933 -3600
# Node ID 234f1730582d5471be003cbfe260783feace9895
# Parent  bce11e8074887f900f2a3eff095b2d91187b70b0
more abstract class Document.Node;

diff -r bce11e807488 -r 234f1730582d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 26 16:58:28 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 17:15:33 2012 +0100
@@ -82,8 +82,6 @@
         case exn => exn
       }
 
-    val empty: Node = Node()
-
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -94,17 +92,31 @@
         (command, start)
       }
     }
+
+    private val block_size = 1024
+
+    val empty: Node = new Node()
   }
 
-  private val block_size = 1024
-
-  sealed case class Node(
+  class Node private(
     val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
     val perspective: Command.Perspective = Command.Perspective.empty,
     val blobs: Map[String, Blob] = Map.empty,
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
-    def clear: Node = Node.empty.copy(header = header)
+    def clear: Node = new Node(header = header)
+
+    def update_header(new_header: Node_Header): Node =
+      new Node(new_header, perspective, blobs, commands)
+
+    def update_perspective(new_perspective: Command.Perspective): Node =
+      new Node(header, new_perspective, blobs, commands)
+
+    def update_blobs(new_blobs: Map[String, Blob]): Node =
+      new Node(header, perspective, new_blobs, commands)
+
+    def update_commands(new_commands: Linear_Set[Command]): Node =
+      new Node(header, perspective, blobs, new_commands)
 
 
     /* commands */
@@ -118,7 +130,7 @@
         last_stop = start + command.length
         while (last_stop + 1 > next_block) {
           blocks += (command -> start)
-          next_block += block_size
+          next_block += Node.block_size
         }
       }
       (blocks.toArray, Text.Range(0, last_stop))
@@ -129,7 +141,7 @@
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
     {
       if (!commands.isEmpty && full_range.contains(i)) {
-        val (cmd0, start0) = full_index._1(i / block_size)
+        val (cmd0, start0) = full_index._1(i / Node.block_size)
         Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
           case (cmd, start) => start + cmd.length <= i }
       }
diff -r bce11e807488 -r 234f1730582d src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 16:58:28 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:15:33 2012 +0100
@@ -135,7 +135,7 @@
     val perspective = command_perspective(node, text_perspective)
     val new_nodes =
       if (node.perspective same perspective) None
-      else Some(nodes + (name -> node.copy(perspective = perspective)))
+      else Some(nodes + (name -> node.update_perspective(perspective)))
     (perspective, new_nodes)
   }
 
@@ -252,7 +252,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
-          nodes += (name -> node.copy(commands = commands2))
+          nodes += (name -> node.update_commands(commands2))
 
         case (name, Document.Node.Header(header)) =>
           val node = nodes(name)
@@ -263,7 +263,7 @@
             }
           if (update_header) {
             doc_edits += (name -> Document.Node.Header(header))
-            nodes += (name -> node.copy(header = header))
+            nodes += (name -> node.update_header(header))
           }
 
         case (name, Document.Node.Perspective(text_perspective)) =>