equal
deleted
inserted
replaced
37 |
37 |
38 type Node_Header = Exn.Result[Thy_Header] |
38 type Node_Header = Exn.Result[Thy_Header] |
39 |
39 |
40 object Node |
40 object Node |
41 { |
41 { |
|
42 object Name |
|
43 { |
|
44 val empty = Name("", "", "") |
|
45 } |
42 sealed case class Name(node: String, dir: String, theory: String) |
46 sealed case class Name(node: String, dir: String, theory: String) |
43 { |
47 { |
44 override def hashCode: Int = node.hashCode |
48 override def hashCode: Int = node.hashCode |
45 override def equals(that: Any): Boolean = |
49 override def equals(that: Any): Boolean = |
46 that match { |
50 that match { |