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