# HG changeset patch
# User wenzelm
# Date 1314197388 -7200
# Node ID 35d67b2056cc55199bbe3ca392fd71eadced6b55
# Parent  cb18e4f09053a70bf4bf11f75487486f20569c00
clarified Document.Node.clear -- retain header (cf. ML version);

diff -r cb18e4f09053 -r 35d67b2056cc src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 24 16:27:27 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 24 16:49:48 2011 +0200
@@ -82,6 +82,9 @@
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
+    def clear: Node = Node.empty.copy(header = header)
+
+
     /* commands */
 
     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
diff -r cb18e4f09053 -r 35d67b2056cc src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 16:27:27 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 16:49:48 2011 +0200
@@ -232,7 +232,7 @@
       edits foreach {
         case (name, Document.Node.Clear()) =>
           doc_edits += (name -> Document.Node.Clear())
-          nodes -= name
+          nodes += (name -> nodes(name).clear)
 
         case (name, Document.Node.Edits(text_edits)) =>
           val node = nodes(name)