clarified Document.Node.clear -- retain header (cf. ML version);
authorwenzelm
Wed Aug 24 16:49:48 2011 +0200 (2011-08-24)
changeset 4444335d67b2056cc
parent 44442 cb18e4f09053
child 44444 33a5616a7571
clarified Document.Node.clear -- retain header (cf. ML version);
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 24 16:27:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 24 16:49:48 2011 +0200
     1.3 @@ -82,6 +82,9 @@
     1.4      val blobs: Map[String, Blob],
     1.5      val commands: Linear_Set[Command])
     1.6    {
     1.7 +    def clear: Node = Node.empty.copy(header = header)
     1.8 +
     1.9 +
    1.10      /* commands */
    1.11  
    1.12      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 16:27:27 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 16:49:48 2011 +0200
     2.3 @@ -232,7 +232,7 @@
     2.4        edits foreach {
     2.5          case (name, Document.Node.Clear()) =>
     2.6            doc_edits += (name -> Document.Node.Clear())
     2.7 -          nodes -= name
     2.8 +          nodes += (name -> nodes(name).clear)
     2.9  
    2.10          case (name, Document.Node.Edits(text_edits)) =>
    2.11            val node = nodes(name)