src/Pure/PIDE/document.scala
changeset 44957 098dd95349e7
parent 44676 7de87f1ae965
child 44959 9476c856c4b9
--- a/src/Pure/PIDE/document.scala	Sat Sep 17 19:55:32 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 17 21:28:52 2011 +0200
@@ -39,6 +39,10 @@
 
   object Node
   {
+    object Name
+    {
+      val empty = Name("", "", "")
+    }
     sealed case class Name(node: String, dir: String, theory: String)
     {
       override def hashCode: Int = node.hashCode