equal
deleted
inserted
replaced
160 |
160 |
161 /* tooltips */ |
161 /* tooltips */ |
162 |
162 |
163 def gui_name(name: String, kind: String = "", prefix: String = ""): String = |
163 def gui_name(name: String, kind: String = "", prefix: String = ""): String = |
164 GUI.Name(name, kind = Word.informal(kind), prefix = prefix, |
164 GUI.Name(name, kind = Word.informal(kind), prefix = prefix, |
165 style = GUI.Style.symbol_decoded).toString |
165 style = GUI.Style_Symbol_Decoded).toString |
166 |
166 |
167 def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name) |
167 def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name) |
168 |
168 |
169 private val tooltip_description = |
169 private val tooltip_description = |
170 Map( |
170 Map( |