src/Pure/PIDE/document.scala
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) =