equal
deleted
inserted
replaced
80 } |
80 } |
81 |
81 |
82 def message(msg: String, theory_name: String, name: String): String = |
82 def message(msg: String, theory_name: String, name: String): String = |
83 msg + " " + quote(name) + " for theory " + quote(theory_name) |
83 msg + " " + quote(name) + " for theory " + quote(theory_name) |
84 |
84 |
85 def compound_name(a: String, b: String): String = a + ":" + b |
85 def compound_name(a: String, b: String): String = |
|
86 if (a.isEmpty) b else a + ":" + b |
86 |
87 |
87 def empty_entry(theory_name: String, name: String): Entry = |
88 def empty_entry(theory_name: String, name: String): Entry = |
88 Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none) |
89 Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none) |
89 |
90 |
90 sealed case class Entry( |
91 sealed case class Entry( |