equal
deleted
inserted
replaced
115 } |
115 } |
116 |
116 |
117 def loaded_theory: Name = Name(theory, "", theory) |
117 def loaded_theory: Name = Name(theory, "", theory) |
118 def is_theory: Boolean = theory.nonEmpty |
118 def is_theory: Boolean = theory.nonEmpty |
119 |
119 |
120 def theory_qualifier: String = Long_Name.qualifier(theory) |
|
121 def theory_base_name: String = Long_Name.base_name(theory) |
120 def theory_base_name: String = Long_Name.base_name(theory) |
122 |
121 |
123 override def toString: String = if (is_theory) theory else node |
122 override def toString: String = if (is_theory) theory else node |
124 |
123 |
125 def map(f: String => String): Name = copy(f(node), f(master_dir), theory) |
124 def map(f: String => String): Name = copy(f(node), f(master_dir), theory) |