changeset 44443 | 35d67b2056cc |
parent 44442 | cb18e4f09053 |
child 44446 | f9334afb6945 |
--- 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) =