1.1 --- a/src/Pure/General/symbol.scala Wed Jul 06 23:11:59 2011 +0200
1.2 +++ b/src/Pure/General/symbol.scala Thu Jul 07 13:48:30 2011 +0200
1.3 @@ -85,7 +85,7 @@
1.4 }
1.5
1.6
1.7 - /* efficient iterators */
1.8 + /* iterator */
1.9
1.10 private val char_symbols: Array[String] =
1.11 (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
1.12 @@ -203,9 +203,13 @@
1.13
1.14
1.15
1.16 - /** Symbol interpretation **/
1.17 + /** symbol interpretation **/
1.18
1.19 - class Interpretation(symbol_decls: List[String])
1.20 + private lazy val symbols =
1.21 + new Interpretation(
1.22 + Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
1.23 +
1.24 + private class Interpretation(symbols_spec: String)
1.25 {
1.26 /* read symbols */
1.27
1.28 @@ -233,7 +237,7 @@
1.29
1.30 private val symbols: List[(String, Map[String, String])] =
1.31 Map((
1.32 - for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
1.33 + for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
1.34 yield read_decl(decl)): _*) toList
1.35
1.36
1.37 @@ -299,12 +303,10 @@
1.38 val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
1.39 val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
1.40
1.41 - def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
1.42 -
1.43
1.44 /* classification */
1.45
1.46 - private val letters = recode_set(
1.47 + val letters = recode_set(
1.48 "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
1.49 "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
1.50 "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
1.51 @@ -339,37 +341,20 @@
1.52
1.53 "\\<^isub>", "\\<^isup>")
1.54
1.55 - private val blanks =
1.56 + val blanks =
1.57 recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
1.58
1.59 - private val sym_chars =
1.60 + val sym_chars =
1.61 Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
1.62
1.63 - def is_letter(sym: String): Boolean = letters.contains(sym)
1.64 - def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
1.65 - def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
1.66 - def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
1.67 - def is_blank(sym: String): Boolean = blanks.contains(sym)
1.68 - def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
1.69 - def is_symbolic(sym: String): Boolean =
1.70 - sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
1.71 -
1.72
1.73 /* control symbols */
1.74
1.75 - private val ctrl_decoded: Set[String] =
1.76 + val ctrl_decoded: Set[String] =
1.77 Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
1.78
1.79 - def is_ctrl(sym: String): Boolean =
1.80 - sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
1.81 -
1.82 - def is_controllable(sym: String): Boolean =
1.83 - !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
1.84 -
1.85 - private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
1.86 - private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
1.87 - def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
1.88 - def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
1.89 + val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
1.90 + val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
1.91
1.92 val bold_decoded = decode("\\<^bold>")
1.93 val bsub_decoded = decode("\\<^bsub>")
1.94 @@ -377,4 +362,47 @@
1.95 val bsup_decoded = decode("\\<^bsup>")
1.96 val esup_decoded = decode("\\<^esup>")
1.97 }
1.98 +
1.99 +
1.100 + /* tables */
1.101 +
1.102 + def names: Map[String, String] = symbols.names
1.103 + def abbrevs: Map[String, String] = symbols.abbrevs
1.104 +
1.105 + def decode(text: String): String = symbols.decode(text)
1.106 + def encode(text: String): String = symbols.encode(text)
1.107 +
1.108 + def fonts: Map[String, String] = symbols.fonts
1.109 + def font_names: List[String] = symbols.font_names
1.110 + def font_index: Map[String, Int] = symbols.font_index
1.111 + def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
1.112 +
1.113 +
1.114 + /* classification */
1.115 +
1.116 + def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
1.117 + def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
1.118 + def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
1.119 + def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
1.120 + def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
1.121 + def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
1.122 + def is_symbolic(sym: String): Boolean =
1.123 + sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
1.124 +
1.125 +
1.126 + /* control symbols */
1.127 +
1.128 + def is_ctrl(sym: String): Boolean =
1.129 + sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
1.130 +
1.131 + def is_controllable(sym: String): Boolean =
1.132 + !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
1.133 +
1.134 + def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
1.135 + def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
1.136 + def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
1.137 + def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
1.138 + def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
1.139 + def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
1.140 + def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
1.141 }