equal
deleted
inserted
replaced
122 |
122 |
123 override def toString: String = if (is_theory) theory else node |
123 override def toString: String = if (is_theory) theory else node |
124 |
124 |
125 def map(f: String => String): Name = copy(f(node), f(master_dir), theory) |
125 def map(f: String => String): Name = copy(f(node), f(master_dir), theory) |
126 def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) |
126 def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) |
|
127 } |
|
128 |
|
129 sealed case class Entry(name: Node.Name, header: Node.Header) |
|
130 { |
|
131 override def toString: String = name.toString |
127 } |
132 } |
128 |
133 |
129 |
134 |
130 /* node overlays */ |
135 /* node overlays */ |
131 |
136 |