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