1.1 --- a/src/Pure/General/scan.scala	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/Pure/General/scan.scala	Thu Jul 07 13:48:30 2011 +0200
     1.3 @@ -335,11 +335,11 @@
     1.4        string | (alt_string | (verb | cmt))
     1.5      }
     1.6  
     1.7 -    private def other_token(symbols: Symbol.Interpretation, is_command: String => Boolean)
     1.8 +    private def other_token(is_command: String => Boolean)
     1.9        : Parser[Token] =
    1.10      {
    1.11 -      val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
    1.12 -      val nat = many1(symbols.is_digit)
    1.13 +      val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y }
    1.14 +      val nat = many1(Symbol.is_digit)
    1.15        val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
    1.16        val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
    1.17  
    1.18 @@ -355,14 +355,14 @@
    1.19          ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
    1.20  
    1.21        val sym_ident =
    1.22 -        (many1(symbols.is_symbolic_char) | one(sym => symbols.is_symbolic(sym))) ^^
    1.23 +        (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
    1.24          (x => Token(Token.Kind.SYM_IDENT, x))
    1.25  
    1.26 -      val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
    1.27 +      val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
    1.28  
    1.29        // FIXME check
    1.30 -      val junk = many(sym => !(symbols.is_blank(sym)))
    1.31 -      val junk1 = many1(sym => !(symbols.is_blank(sym)))
    1.32 +      val junk = many(sym => !(Symbol.is_blank(sym)))
    1.33 +      val junk1 = many1(sym => !(Symbol.is_blank(sym)))
    1.34  
    1.35        val bad_delimiter =
    1.36          ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) }
    1.37 @@ -376,11 +376,10 @@
    1.38            command_keyword) | bad))
    1.39      }
    1.40  
    1.41 -    def token(symbols: Symbol.Interpretation, is_command: String => Boolean): Parser[Token] =
    1.42 -      delimited_token | other_token(symbols, is_command)
    1.43 +    def token(is_command: String => Boolean): Parser[Token] =
    1.44 +      delimited_token | other_token(is_command)
    1.45  
    1.46 -    def token_context(symbols: Symbol.Interpretation, is_command: String => Boolean, ctxt: Context)
    1.47 -      : Parser[(Token, Context)] =
    1.48 +    def token_context(is_command: String => Boolean, ctxt: Context): Parser[(Token, Context)] =
    1.49      {
    1.50        val string =
    1.51          quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
    1.52 @@ -388,7 +387,7 @@
    1.53          quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
    1.54        val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
    1.55        val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
    1.56 -      val other = other_token(symbols, is_command) ^^ { case x => (x, Finished) }
    1.57 +      val other = other_token(is_command) ^^ { case x => (x, Finished) }
    1.58  
    1.59        string | (alt_string | (verb | (cmt | other)))
    1.60      }

     2.1 --- a/src/Pure/General/symbol.scala	Wed Jul 06 23:11:59 2011 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Thu Jul 07 13:48:30 2011 +0200
     2.3 @@ -85,7 +85,7 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* efficient iterators */
     2.8 +  /* iterator */
     2.9  
    2.10    private val char_symbols: Array[String] =
    2.11      (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
    2.12 @@ -203,9 +203,13 @@
    2.13  
    2.14  
    2.15  
    2.16 -  /** Symbol interpretation **/
    2.17 +  /** symbol interpretation **/
    2.18  
    2.19 -  class Interpretation(symbol_decls: List[String])
    2.20 +  private lazy val symbols =
    2.21 +    new Interpretation(
    2.22 +      Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
    2.23 +
    2.24 +  private class Interpretation(symbols_spec: String)
    2.25    {
    2.26      /* read symbols */
    2.27  
    2.28 @@ -233,7 +237,7 @@
    2.29  
    2.30      private val symbols: List[(String, Map[String, String])] =
    2.31        Map((
    2.32 -        for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
    2.33 +        for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
    2.34            yield read_decl(decl)): _*) toList
    2.35  
    2.36  
    2.37 @@ -299,12 +303,10 @@
    2.38      val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    2.39      val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
    2.40  
    2.41 -    def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
    2.42 -
    2.43  
    2.44      /* classification */
    2.45  
    2.46 -    private val letters = recode_set(
    2.47 +    val letters = recode_set(
    2.48        "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
    2.49        "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
    2.50        "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
    2.51 @@ -339,37 +341,20 @@
    2.52  
    2.53        "\\<^isub>", "\\<^isup>")
    2.54  
    2.55 -    private val blanks =
    2.56 +    val blanks =
    2.57        recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
    2.58  
    2.59 -    private val sym_chars =
    2.60 +    val sym_chars =
    2.61        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
    2.62  
    2.63 -    def is_letter(sym: String): Boolean = letters.contains(sym)
    2.64 -    def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
    2.65 -    def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
    2.66 -    def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
    2.67 -    def is_blank(sym: String): Boolean = blanks.contains(sym)
    2.68 -    def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
    2.69 -    def is_symbolic(sym: String): Boolean =
    2.70 -      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
    2.71 -
    2.72  
    2.73      /* control symbols */
    2.74  
    2.75 -    private val ctrl_decoded: Set[String] =
    2.76 +    val ctrl_decoded: Set[String] =
    2.77        Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
    2.78  
    2.79 -    def is_ctrl(sym: String): Boolean =
    2.80 -      sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
    2.81 -
    2.82 -    def is_controllable(sym: String): Boolean =
    2.83 -      !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
    2.84 -
    2.85 -    private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    2.86 -    private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
    2.87 -    def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
    2.88 -    def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
    2.89 +    val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    2.90 +    val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
    2.91  
    2.92      val bold_decoded = decode("\\<^bold>")
    2.93      val bsub_decoded = decode("\\<^bsub>")
    2.94 @@ -377,4 +362,47 @@
    2.95      val bsup_decoded = decode("\\<^bsup>")
    2.96      val esup_decoded = decode("\\<^esup>")
    2.97    }
    2.98 +
    2.99 +
   2.100 +  /* tables */
   2.101 +
   2.102 +  def names: Map[String, String] = symbols.names
   2.103 +  def abbrevs: Map[String, String] = symbols.abbrevs
   2.104 +
   2.105 +  def decode(text: String): String = symbols.decode(text)
   2.106 +  def encode(text: String): String = symbols.encode(text)
   2.107 +
   2.108 +  def fonts: Map[String, String] = symbols.fonts
   2.109 +  def font_names: List[String] = symbols.font_names
   2.110 +  def font_index: Map[String, Int] = symbols.font_index
   2.111 +  def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
   2.112 +
   2.113 +
   2.114 +  /* classification */
   2.115 +
   2.116 +  def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
   2.117 +  def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   2.118 +  def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
   2.119 +  def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   2.120 +  def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
   2.121 +  def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
   2.122 +  def is_symbolic(sym: String): Boolean =
   2.123 +    sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
   2.124 +
   2.125 +
   2.126 +  /* control symbols */
   2.127 +
   2.128 +  def is_ctrl(sym: String): Boolean =
   2.129 +    sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
   2.130 +
   2.131 +  def is_controllable(sym: String): Boolean =
   2.132 +    !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
   2.133 +
   2.134 +  def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
   2.135 +  def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
   2.136 +  def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
   2.137 +  def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
   2.138 +  def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
   2.139 +  def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
   2.140 +  def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
   2.141  }

     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 06 23:11:59 2011 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Jul 07 13:48:30 2011 +0200
     3.3 @@ -11,11 +11,11 @@
     3.4  import scala.collection.mutable
     3.5  
     3.6  
     3.7 -class Outer_Syntax(symbols: Symbol.Interpretation)
     3.8 +class Outer_Syntax
     3.9  {
    3.10    protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
    3.11    protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    3.12 -  lazy val completion: Completion = new Completion + symbols // FIXME odd initialization
    3.13 +  lazy val completion: Completion = (new Completion).add_symbols // FIXME odd initialization
    3.14  
    3.15    def keyword_kind(name: String): Option[String] = keywords.get(name)
    3.16  
    3.17 @@ -24,7 +24,7 @@
    3.18      val new_keywords = keywords + (name -> kind)
    3.19      val new_lexicon = lexicon + name
    3.20      val new_completion = completion + (name, replace)
    3.21 -    new Outer_Syntax(symbols) {
    3.22 +    new Outer_Syntax {
    3.23        override val lexicon = new_lexicon
    3.24        override val keywords = new_keywords
    3.25        override lazy val completion = new_completion
    3.26 @@ -66,7 +66,7 @@
    3.27    {
    3.28      import lexicon._
    3.29  
    3.30 -    parseAll(rep(token(symbols, is_command)), input) match {
    3.31 +    parseAll(rep(token(is_command)), input) match {
    3.32        case Success(tokens, _) => tokens
    3.33        case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    3.34      }
    3.35 @@ -83,7 +83,7 @@
    3.36      val toks = new mutable.ListBuffer[Token]
    3.37      var ctxt = context
    3.38      while (!in.atEnd) {
    3.39 -      parse(token_context(symbols, is_command, ctxt), in) match {
    3.40 +      parse(token_context(is_command, ctxt), in) match {
    3.41          case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    3.42          case NoSuccess(_, rest) =>
    3.43            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)

     4.1 --- a/src/Pure/System/isabelle_process.scala	Wed Jul 06 23:11:59 2011 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Jul 07 13:48:30 2011 +0200
     4.3 @@ -92,7 +92,7 @@
     4.4  
     4.5    private def put_result(kind: String, text: String)
     4.6    {
     4.7 -    put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
     4.8 +    put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
     4.9    }
    4.10  
    4.11  
    4.12 @@ -341,7 +341,7 @@
    4.13  
    4.14          if (i != n) throw new Protocol_Error("bad message chunk content")
    4.15  
    4.16 -        YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
    4.17 +        YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
    4.18          //}}}
    4.19        }
    4.20  

     5.1 --- a/src/Pure/System/isabelle_system.scala	Wed Jul 06 23:11:59 2011 +0200
     5.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jul 07 13:48:30 2011 +0200
     5.3 @@ -1,8 +1,8 @@
     5.4  /*  Title:      Pure/System/isabelle_system.scala
     5.5      Author:     Makarius
     5.6  
     5.7 -Fundamental Isabelle system environment: settings, symbols etc.
     5.8 -Quasi-static module with optional init operation.
     5.9 +Fundamental Isabelle system environment: quasi-static module with
    5.10 +optional init operation.
    5.11  */
    5.12  
    5.13  package isabelle
    5.14 @@ -24,10 +24,7 @@
    5.15  {
    5.16    /** implicit state **/
    5.17  
    5.18 -  private case class State(
    5.19 -    standard_system: Standard_System,
    5.20 -    settings: Map[String, String],
    5.21 -    symbols: Symbol.Interpretation)
    5.22 +  private case class State(standard_system: Standard_System, settings: Map[String, String])
    5.23  
    5.24    @volatile private var _state: Option[State] = None
    5.25  
    5.26 @@ -39,7 +36,6 @@
    5.27  
    5.28    def standard_system: Standard_System = check_state().standard_system
    5.29    def settings: Map[String, String] = check_state().settings
    5.30 -  def symbols: Symbol.Interpretation = check_state().symbols
    5.31  
    5.32    /*
    5.33      isabelle_home precedence:
    5.34 @@ -51,8 +47,9 @@
    5.35      if (_state.isEmpty) {
    5.36        import scala.collection.JavaConversions._
    5.37  
    5.38 +      System.err.println("### Isabelle system initialization")
    5.39 +
    5.40        val standard_system = new Standard_System
    5.41 -
    5.42        val settings =
    5.43        {
    5.44          val env = Map(System.getenv.toList: _*) +
    5.45 @@ -89,17 +86,7 @@
    5.46                  ("PATH" -> System.getenv("PATH"))
    5.47              }
    5.48            }
    5.49 -
    5.50 -      val symbols =
    5.51 -      {
    5.52 -        val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
    5.53 -        if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
    5.54 -        val files =
    5.55 -          Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
    5.56 -        new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
    5.57 -      }
    5.58 -
    5.59 -      _state = Some(State(standard_system, settings, symbols))
    5.60 +      _state = Some(State(standard_system, settings))
    5.61      }
    5.62    }
    5.63  

     6.1 --- a/src/Pure/System/session.scala	Wed Jul 06 23:11:59 2011 +0200
     6.2 +++ b/src/Pure/System/session.scala	Thu Jul 07 13:48:30 2011 +0200
     6.3 @@ -117,7 +117,7 @@
     6.4  
     6.5    @volatile var loaded_theories: Set[String] = Set()
     6.6  
     6.7 -  @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
     6.8 +  @volatile private var syntax = new Outer_Syntax
     6.9    def current_syntax(): Outer_Syntax = syntax
    6.10  
    6.11    @volatile private var reverse_syslog = List[XML.Elem]()
    6.12 @@ -202,9 +202,7 @@
    6.13                        case Some(command) =>
    6.14                          if (global_state.peek().lookup_command(command.id).isEmpty) {
    6.15                            global_state.change(_.define_command(command))
    6.16 -                          prover.get.
    6.17 -                            define_command(command.id,
    6.18 -                              Isabelle_System.symbols.encode(command.source))
    6.19 +                          prover.get.define_command(command.id, Symbol.encode(command.source))
    6.20                          }
    6.21                          Some(command.id)
    6.22                      }

     7.1 --- a/src/Pure/System/standard_system.scala	Wed Jul 06 23:11:59 2011 +0200
     7.2 +++ b/src/Pure/System/standard_system.scala	Thu Jul 07 13:48:30 2011 +0200
     7.3 @@ -96,16 +96,6 @@
     7.4  
     7.5    def read_file(file: File): String = slurp(new FileInputStream(file))
     7.6  
     7.7 -  def try_read(files: Seq[File]): String =
     7.8 -  {
     7.9 -    val buf = new StringBuilder
    7.10 -    for {
    7.11 -      file <- files if file.isFile
    7.12 -      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
    7.13 -    } buf.append(c)
    7.14 -    buf.toString
    7.15 -  }
    7.16 -
    7.17    def write_file(file: File, text: CharSequence)
    7.18    {
    7.19      val writer =

     8.1 --- a/src/Pure/Thy/completion.scala	Wed Jul 06 23:11:59 2011 +0200
     8.2 +++ b/src/Pure/Thy/completion.scala	Thu Jul 07 13:48:30 2011 +0200
     8.3 @@ -62,15 +62,15 @@
     8.4  
     8.5    def + (keyword: String): Completion = this + (keyword, keyword)
     8.6  
     8.7 -  def + (symbols: Symbol.Interpretation): Completion =
     8.8 +  def add_symbols: Completion =
     8.9    {
    8.10      val words =
    8.11 -      (for ((x, _) <- symbols.names) yield (x, x)).toList :::
    8.12 -      (for ((x, y) <- symbols.names) yield (y, x)).toList :::
    8.13 -      (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
    8.14 +      (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
    8.15 +      (for ((x, y) <- Symbol.names) yield (y, x)).toList :::
    8.16 +      (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
    8.17  
    8.18      val abbrs =
    8.19 -      (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
    8.20 +      (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
    8.21          yield (y.reverse.toString, (y, x))).toList
    8.22  
    8.23      val old = this

     9.1 --- a/src/Pure/Thy/html.scala	Wed Jul 06 23:11:59 2011 +0200
     9.2 +++ b/src/Pure/Thy/html.scala	Thu Jul 07 13:48:30 2011 +0200
     9.3 @@ -57,8 +57,6 @@
     9.4  
     9.5    def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
     9.6    {
     9.7 -    val symbols = Isabelle_System.symbols
     9.8 -
     9.9      def html_spans(tree: XML.Tree): XML.Body =
    9.10        tree match {
    9.11          case XML.Elem(m @ Markup(name, props), ts) =>
    9.12 @@ -85,14 +83,14 @@
    9.13              val s1 = syms.next
    9.14              def s2() = if (syms.hasNext) syms.next else ""
    9.15              if (s1 == "\n") add(XML.elem(BR))
    9.16 -            else if (s1 == symbols.bsub_decoded) t ++= s1  // FIXME
    9.17 -            else if (s1 == symbols.esub_decoded) t ++= s1  // FIXME
    9.18 -            else if (s1 == symbols.bsup_decoded) t ++= s1  // FIXME
    9.19 -            else if (s1 == symbols.esup_decoded) t ++= s1  // FIXME
    9.20 -            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    9.21 -            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    9.22 -            else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
    9.23 -            else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
    9.24 +            else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
    9.25 +            else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
    9.26 +            else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
    9.27 +            else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
    9.28 +            else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    9.29 +            else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    9.30 +            else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    9.31 +            else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
    9.32              else t ++= s1
    9.33            }
    9.34            flush()

    10.1 --- a/src/Pure/Thy/thy_header.scala	Wed Jul 06 23:11:59 2011 +0200
    10.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jul 07 13:48:30 2011 +0200
    10.3 @@ -75,7 +75,7 @@
    10.4  
    10.5    def read(reader: Reader[Char]): Header =
    10.6    {
    10.7 -    val token = lexicon.token(Isabelle_System.symbols, _ => false)
    10.8 +    val token = lexicon.token(_ => false)
    10.9      val toks = new mutable.ListBuffer[Token]
   10.10  
   10.11      @tailrec def scan_to_begin(in: Reader[Char])

    11.1 --- a/src/Pure/build-jars	Wed Jul 06 23:11:59 2011 +0200
    11.2 +++ b/src/Pure/build-jars	Thu Jul 07 13:48:30 2011 +0200
    11.3 @@ -138,9 +138,7 @@
    11.4  
    11.5  if [ "$OUTDATED" = true ]
    11.6  then
    11.7 -  echo "###"
    11.8    echo "### Building Isabelle/Scala layer ..."
    11.9 -  echo "###"
   11.10  
   11.11    [ "${#UPDATED[@]}" -gt 0 ] && {
   11.12      echo "Changed files:"

    12.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jul 06 23:11:59 2011 +0200
    12.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jul 07 13:48:30 2011 +0200
    12.3 @@ -202,9 +202,7 @@
    12.4  
    12.5  if [ "$OUTDATED" = true ]
    12.6  then
    12.7 -  echo "###"
    12.8    echo "### Building Isabelle/jEdit ..."
    12.9 -  echo "###"
   12.10  
   12.11    [ "${#UPDATED[@]}" -gt 0 ] && {
   12.12      echo "Changed files:"

    13.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Wed Jul 06 23:11:59 2011 +0200
    13.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Jul 07 13:48:30 2011 +0200
    13.3 @@ -34,7 +34,7 @@
    13.4    private def text_reader(in: InputStream, codec: Codec): Reader =
    13.5    {
    13.6      val source = new BufferedSource(in)(codec)
    13.7 -    new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray)
    13.8 +    new CharArrayReader(Symbol.decode(source.mkString).toArray)
    13.9    }
   13.10  
   13.11    override def getTextReader(in: InputStream): Reader =
   13.12 @@ -53,7 +53,7 @@
   13.13      val buffer = new ByteArrayOutputStream(BUFSIZE) {
   13.14        override def flush()
   13.15        {
   13.16 -        val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name))
   13.17 +        val text = Symbol.encode(toString(Standard_System.charset_name))
   13.18          out.write(text.getBytes(Standard_System.charset))
   13.19          out.flush()
   13.20        }

    14.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Jul 06 23:11:59 2011 +0200
    14.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Jul 07 13:48:30 2011 +0200
    14.3 @@ -96,7 +96,7 @@
    14.4              case Some((word, cs)) =>
    14.5                val ds =
    14.6                  (if (Isabelle_Encoding.is_active(buffer))
    14.7 -                  cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
    14.8 +                  cs.map(Symbol.decode(_)).sortWith(_ < _)
    14.9                   else cs).filter(_ != word)
   14.10                if (ds.isEmpty) null
   14.11                else new SideKickCompletion(

    15.1 --- a/src/Tools/jEdit/src/token_markup.scala	Wed Jul 06 23:11:59 2011 +0200
    15.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 13:48:30 2011 +0200
    15.3 @@ -81,9 +81,8 @@
    15.4  
    15.5    class Style_Extender extends SyntaxUtilities.StyleExtender
    15.6    {
    15.7 -    val symbols = Isabelle_System.symbols
    15.8 -    if (symbols.font_names.length > 2)
    15.9 -      error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
   15.10 +    if (Symbol.font_names.length > 2)
   15.11 +      error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
   15.12  
   15.13      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
   15.14      {
   15.15 @@ -94,7 +93,7 @@
   15.16          new_styles(subscript(i.toByte)) = script_style(style, -1)
   15.17          new_styles(superscript(i.toByte)) = script_style(style, 1)
   15.18          new_styles(bold(i.toByte)) = bold_style(style)
   15.19 -        for ((family, idx) <- symbols.font_index)
   15.20 +        for ((family, idx) <- Symbol.font_index)
   15.21            new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
   15.22        }
   15.23        new_styles(hidden) =
   15.24 @@ -108,13 +107,11 @@
   15.25  
   15.26    def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   15.27    {
   15.28 -    val symbols = Isabelle_System.symbols
   15.29 -
   15.30 -    // FIXME symbols.bsub_decoded etc.
   15.31 +    // FIXME Symbol.is_bsub_decoded etc.
   15.32      def ctrl_style(sym: String): Option[Byte => Byte] =
   15.33 -      if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
   15.34 -      else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
   15.35 -      else if (sym == symbols.bold_decoded) Some(bold(_))
   15.36 +      if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
   15.37 +      else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
   15.38 +      else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
   15.39        else None
   15.40  
   15.41      var result = Map[Text.Offset, Byte => Byte]()
   15.42 @@ -127,13 +124,13 @@
   15.43      for (sym <- Symbol.iterator(text)) {
   15.44        if (ctrl_style(sym).isDefined) ctrl = sym
   15.45        else if (ctrl != "") {
   15.46 -        if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
   15.47 +        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
   15.48            mark(offset - ctrl.length, offset, _ => hidden)
   15.49            mark(offset, offset + sym.length, ctrl_style(ctrl).get)
   15.50          }
   15.51          ctrl = ""
   15.52        }
   15.53 -      symbols.lookup_font(sym) match {
   15.54 +      Symbol.lookup_font(sym) match {
   15.55          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
   15.56          case _ =>
   15.57        }