wneuper/isa: comparison src/Pure/General/symbol.scala

equal deleted inserted replaced

-:93dcfcf91484
+:5130dfe1b7be
 }
 }
 }
-/* efficient iterators */
+/* iterator */
 private val char_symbols: Array[String] =
 (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
 def iterator(text: CharSequence): Iterator[String] =
 }
 }
-/** Symbol interpretation **/
+/** symbol interpretation **/
-class Interpretation(symbol_decls: List[String])
+private lazy val symbols =
+new Interpretation(
+Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
+private class Interpretation(symbols_spec: String)
 {
 /* read symbols */
 private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
 private val key = new Regex("""(?xs) (.+): """)
 }
 }
 private val symbols: List[(String, Map[String, String])] =
 Map((
-for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
+for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
 yield read_decl(decl)): _*) toList
 /* misc properties */
 yield (sym -> props("font"))): _*)
 val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
 val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
-def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
 /* classification */
-private val letters = recode_set(
+val letters = recode_set(
 "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
 "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
 "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
 "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
 "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
 "\\<Psi>", "\\<Omega>",
 "\\<^isub>", "\\<^isup>")
-private val blanks =
+val blanks =
 recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
-private val sym_chars =
+val sym_chars =
 Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
-def is_letter(sym: String): Boolean = letters.contains(sym)
-def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
-def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
-def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
-def is_blank(sym: String): Boolean = blanks.contains(sym)
-def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
-def is_symbolic(sym: String): Boolean =
-sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 /* control symbols */
-private val ctrl_decoded: Set[String] =
+val ctrl_decoded: Set[String] =
 Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
-def is_ctrl(sym: String): Boolean =
+val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
-sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
+val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-def is_controllable(sym: String): Boolean =
-!is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
-private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
-private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
-def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
 val bold_decoded = decode("\\<^bold>")
 val bsub_decoded = decode("\\<^bsub>")
 val esub_decoded = decode("\\<^esub>")
 val bsup_decoded = decode("\\<^bsup>")
 val esup_decoded = decode("\\<^esup>")
 }
+/* tables */
+def names: Map[String, String] = symbols.names
+def abbrevs: Map[String, String] = symbols.abbrevs
+def decode(text: String): String = symbols.decode(text)
+def encode(text: String): String = symbols.encode(text)
+def fonts: Map[String, String] = symbols.fonts
+def font_names: List[String] = symbols.font_names
+def font_index: Map[String, Int] = symbols.font_index
+def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
+/* classification */
+def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
+def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
+def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
+def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
+def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
+def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
+def is_symbolic(sym: String): Boolean =
+sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
+/* control symbols */
+def is_ctrl(sym: String): Boolean =
+sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
+def is_controllable(sym: String): Boolean =
+!is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
+def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
+def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
+def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
+def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
+def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
+def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
+def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
 }

changeset 44569	5130dfe1b7be
parent 44550	8252d51d70e2
child 44570	58bb7ca5c7a2