src/Pure/PIDE/document.scala
changeset 44616 4beeaf2a226d
parent 44615 a4ff8a787202
child 44642 446fe2abe252
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Sep 01 13:34:45 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Sep 01 13:39:40 2011 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  
     1.5    object Node
     1.6    {
     1.7 -    sealed case class Name(node: String, master_dir: String, theory: String)
     1.8 +    sealed case class Name(node: String, dir: String, theory: String)
     1.9      {
    1.10        override def hashCode: Int = node.hashCode
    1.11        override def equals(that: Any): Boolean =