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) =