1 /* Title: Pure/General/symbol.scala
5 Detecting and recoding Isabelle symbols.
10 import java.util.regex.Pattern
12 import scala.io.Source
13 import scala.collection.jcl.HashMap
18 /** Symbol regexps **/
20 private def compile(s: String) =
21 Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
23 private val plain_pattern = compile(""" [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
25 private val symbol_pattern = compile(""" \\ \\? < (?:
26 \^? [A-Za-z][A-Za-z0-9_']* |
27 \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
29 private val bad_symbol_pattern = compile("(?!" + symbol_pattern + ")" +
30 """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
33 val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| .")
39 private class Recoder(list: List[(String, String)]) {
40 private val (min, max) = {
43 for ((x, _) <- list) {
51 val table = new HashMap[String, String]
52 for ((x, y) <- list) table + (x -> y)
55 def recode(text: String) = {
57 val matcher = pattern.matcher(text)
58 val result = new StringBuilder(len)
62 if (min <= c && c <= max) {
63 matcher.region(i, len)
67 case Some(y) => result.append(y)
68 case None => result.append(x)
72 else { result.append(c); i += 1 }
80 /** Symbol interpretation **/
82 class Interpretation {
84 private var symbols = new HashMap[String, HashMap[String, String]]
85 private var decoder: Recoder = null
86 private var encoder: Recoder = null
88 def decode(text: String) = decoder.recode(text)
89 def encode(text: String) = encoder.recode(text)
94 private val empty_pattern = compile(""" ^\s* (?: \#.* )? $ """)
95 private val blank_pattern = compile(""" \s+ """)
96 private val key_pattern = compile(""" (.+): """)
98 private def read_line(line: String) = {
99 def err() = error("Bad symbol specification (line " + line + ")")
101 def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
104 case _ :: Nil => err()
105 case key :: value :: rest => {
106 val key_matcher = key_pattern.matcher(key)
107 if (key_matcher.matches) {
108 tab + (key_matcher.group(1) -> value)
109 read_props(rest, tab)
116 if (!empty_pattern.matcher(line).matches) {
117 blank_pattern.split(line).toList match {
119 case symbol :: props => {
120 val tab = new HashMap[String, String]
121 read_props(props, tab)
122 symbols + (symbol -> tab)
128 private def read_symbols(path: String) = {
129 val file = new File(IsabelleSystem.platform_path(path))
131 for (line <- Source.fromFile(file).getLines) read_line(line)
138 private def get_code(entry: (String, HashMap[String, String])) = {
139 val (symbol, props) = entry
141 try { Integer.decode(props("code")).intValue }
143 case _: NoSuchElementException => error("Missing code for symbol " + symbol)
144 case _: NumberFormatException => error("Bad code for symbol " + symbol)
146 (symbol, new String(Character.toChars(code)))
149 private def init_recoders() = {
150 val list = symbols.elements.toList.map(get_code)
151 decoder = new Recoder(list ::: (for ((x, y) <- list) yield ("\\" + x, y)))
152 encoder = new Recoder(for ((x, y) <- list) yield (y, x))
158 read_symbols("$ISABELLE_HOME/etc/symbols")
159 read_symbols("$ISABELLE_HOME_USER/etc/symbols")