equal
deleted
inserted
replaced
113 override def equals(that: Any): Boolean = |
113 override def equals(that: Any): Boolean = |
114 that match { |
114 that match { |
115 case other: Name => node == other.node |
115 case other: Name => node == other.node |
116 case _ => false |
116 case _ => false |
117 } |
117 } |
|
118 |
|
119 def path: Path = Path.explode(node) |
118 |
120 |
119 def is_theory: Boolean = theory.nonEmpty |
121 def is_theory: Boolean = theory.nonEmpty |
120 |
122 |
121 def theory_base_name: String = Long_Name.base_name(theory) |
123 def theory_base_name: String = Long_Name.base_name(theory) |
122 |
124 |