equal
deleted
inserted
replaced
81 name: String, |
81 name: String, |
82 executable: Boolean, |
82 executable: Boolean, |
83 body: Future[(Boolean, Bytes)]) |
83 body: Future[(Boolean, Bytes)]) |
84 { |
84 { |
85 override def toString: String = name |
85 override def toString: String = name |
|
86 |
|
87 def compound_name: String = Export.compound_name(theory_name, name) |
86 |
88 |
87 val name_elems: List[String] = explode_name(name) |
89 val name_elems: List[String] = explode_name(name) |
88 |
90 |
89 def name_extends(elems: List[String]): Boolean = |
91 def name_extends(elems: List[String]): Boolean = |
90 name_elems.startsWith(elems) && name_elems != elems |
92 name_elems.startsWith(elems) && name_elems != elems |