src/Pure/Thy/thy_syntax.scala
changeset 44185 05641edb5d30
parent 44182 ecb51b457064
child 44385 e7fdb008aa7d
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 16:07:26 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 20:20:36 2011 +0200
     1.3 @@ -179,8 +179,8 @@
     1.4        var nodes = previous.nodes
     1.5  
     1.6        edits foreach {
     1.7 -        case (name, Document.Node.Remove()) =>
     1.8 -          doc_edits += (name -> Document.Node.Remove())
     1.9 +        case (name, Document.Node.Clear()) =>
    1.10 +          doc_edits += (name -> Document.Node.Clear())
    1.11            nodes -= name
    1.12  
    1.13          case (name, Document.Node.Edits(text_edits)) =>