src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/General/symbol.scala	Thu Jul 07 13:48:30 2011 +0200
@@ -85,7 +85,7 @@
   }
 
 
-  /* efficient iterators */
+  /* iterator */
 
   private val char_symbols: Array[String] =
     (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
@@ -203,9 +203,13 @@
 
 
 
-  /** 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 */
 
@@ -233,7 +237,7 @@
 
     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
 
 
@@ -299,12 +303,10 @@
     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",
@@ -339,37 +341,20 @@
 
       "\\<^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 =
-      sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
-
-    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 subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
+    val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
 
     val bold_decoded = decode("\\<^bold>")
     val bsub_decoded = decode("\\<^bsub>")
@@ -377,4 +362,47 @@
     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
 }