1.1 --- a/src/Pure/General/scan.scala	Thu Jul 07 13:48:30 2011 +0200
     1.2 +++ b/src/Pure/General/scan.scala	Thu Jul 07 14:10:50 2011 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  
     1.5      /* symbol range */
     1.6  
     1.7 -    def symbol_range(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
     1.8 +    def symbol_range(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
     1.9        new Parser[String]
    1.10        {
    1.11          def apply(in: Input) =
    1.12 @@ -187,25 +187,30 @@
    1.13          }
    1.14        }.named("symbol_range")
    1.15  
    1.16 -    def one(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, 1)
    1.17 -    def many(pred: String => Boolean): Parser[String] = symbol_range(pred, 0, Integer.MAX_VALUE)
    1.18 -    def many1(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, Integer.MAX_VALUE)
    1.19 +    def one(pred: Symbol.Symbol => Boolean): Parser[String] =
    1.20 +      symbol_range(pred, 1, 1)
    1.21 +
    1.22 +    def many(pred: Symbol.Symbol => Boolean): Parser[String] =
    1.23 +      symbol_range(pred, 0, Integer.MAX_VALUE)
    1.24 +
    1.25 +    def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
    1.26 +      symbol_range(pred, 1, Integer.MAX_VALUE)
    1.27  
    1.28  
    1.29      /* quoted strings */
    1.30  
    1.31 -    private def quoted_body(quote: String): Parser[String] =
    1.32 +    private def quoted_body(quote: Symbol.Symbol): Parser[String] =
    1.33      {
    1.34        rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
    1.35          (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
    1.36      }
    1.37  
    1.38 -    private def quoted(quote: String): Parser[String] =
    1.39 +    private def quoted(quote: Symbol.Symbol): Parser[String] =
    1.40      {
    1.41        quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
    1.42      }.named("quoted")
    1.43  
    1.44 -    def quoted_content(quote: String, source: String): String =
    1.45 +    def quoted_content(quote: Symbol.Symbol, source: String): String =
    1.46      {
    1.47        require(parseAll(quoted(quote), source).successful)
    1.48        val body = source.substring(1, source.length - 1)
    1.49 @@ -218,7 +223,7 @@
    1.50        else body
    1.51      }
    1.52  
    1.53 -    def quoted_context(quote: String, ctxt: Context): Parser[(String, Context)] =
    1.54 +    def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] =
    1.55      {
    1.56        ctxt match {
    1.57          case Finished =>

     2.1 --- a/src/Pure/General/symbol.scala	Thu Jul 07 13:48:30 2011 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Thu Jul 07 14:10:50 2011 +0200
     2.3 @@ -13,6 +13,9 @@
     2.4  
     2.5  object Symbol
     2.6  {
     2.7 +  type Symbol = String
     2.8 +
     2.9 +
    2.10    /* spaces */
    2.11  
    2.12    val spc = ' '
    2.13 @@ -64,10 +67,10 @@
    2.14  
    2.15    def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
    2.16  
    2.17 -  def is_physical_newline(s: String): Boolean =
    2.18 +  def is_physical_newline(s: Symbol): Boolean =
    2.19      s == "\n" || s == "\r" || s == "\r\n"
    2.20  
    2.21 -  def is_malformed(s: String): Boolean =
    2.22 +  def is_malformed(s: Symbol): Boolean =
    2.23      !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
    2.24  
    2.25    class Matcher(text: CharSequence)
    2.26 @@ -87,11 +90,11 @@
    2.27  
    2.28    /* iterator */
    2.29  
    2.30 -  private val char_symbols: Array[String] =
    2.31 +  private val char_symbols: Array[Symbol] =
    2.32      (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
    2.33  
    2.34 -  def iterator(text: CharSequence): Iterator[String] =
    2.35 -    new Iterator[String]
    2.36 +  def iterator(text: CharSequence): Iterator[Symbol] =
    2.37 +    new Iterator[Symbol]
    2.38      {
    2.39        private val matcher = new Matcher(text)
    2.40        private var i = 0
    2.41 @@ -216,7 +219,7 @@
    2.42      private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
    2.43      private val key = new Regex("""(?xs) (.+): """)
    2.44  
    2.45 -    private def read_decl(decl: String): (String, Map[String, String]) =
    2.46 +    private def read_decl(decl: String): (Symbol, Map[String, String]) =
    2.47      {
    2.48        def err() = error("Bad symbol declaration: " + decl)
    2.49  
    2.50 @@ -235,7 +238,7 @@
    2.51        }
    2.52      }
    2.53  
    2.54 -    private val symbols: List[(String, Map[String, String])] =
    2.55 +    private val symbols: List[(Symbol, Map[String, String])] =
    2.56        Map((
    2.57          for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
    2.58            yield read_decl(decl)): _*) toList
    2.59 @@ -243,13 +246,13 @@
    2.60  
    2.61      /* misc properties */
    2.62  
    2.63 -    val names: Map[String, String] =
    2.64 +    val names: Map[Symbol, String] =
    2.65      {
    2.66        val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
    2.67        Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
    2.68      }
    2.69  
    2.70 -    val abbrevs: Map[String, String] =
    2.71 +    val abbrevs: Map[Symbol, String] =
    2.72        Map((
    2.73          for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
    2.74            yield (sym -> props("abbrev"))): _*)
    2.75 @@ -295,7 +298,7 @@
    2.76  
    2.77      /* user fonts */
    2.78  
    2.79 -    val fonts: Map[String, String] =
    2.80 +    val fonts: Map[Symbol, String] =
    2.81        recode_map((
    2.82          for ((sym, props) <- symbols if props.isDefinedAt("font"))
    2.83            yield (sym -> props("font"))): _*)
    2.84 @@ -350,7 +353,7 @@
    2.85  
    2.86      /* control symbols */
    2.87  
    2.88 -    val ctrl_decoded: Set[String] =
    2.89 +    val ctrl_decoded: Set[Symbol] =
    2.90        Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
    2.91  
    2.92      val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    2.93 @@ -366,43 +369,43 @@
    2.94  
    2.95    /* tables */
    2.96  
    2.97 -  def names: Map[String, String] = symbols.names
    2.98 -  def abbrevs: Map[String, String] = symbols.abbrevs
    2.99 +  def names: Map[Symbol, String] = symbols.names
   2.100 +  def abbrevs: Map[Symbol, String] = symbols.abbrevs
   2.101  
   2.102    def decode(text: String): String = symbols.decode(text)
   2.103    def encode(text: String): String = symbols.encode(text)
   2.104  
   2.105 -  def fonts: Map[String, String] = symbols.fonts
   2.106 +  def fonts: Map[Symbol, String] = symbols.fonts
   2.107    def font_names: List[String] = symbols.font_names
   2.108    def font_index: Map[String, Int] = symbols.font_index
   2.109 -  def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
   2.110 +  def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
   2.111  
   2.112  
   2.113    /* classification */
   2.114  
   2.115 -  def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
   2.116 -  def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   2.117 -  def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
   2.118 -  def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   2.119 -  def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
   2.120 -  def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
   2.121 -  def is_symbolic(sym: String): Boolean =
   2.122 +  def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
   2.123 +  def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
   2.124 +  def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
   2.125 +  def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   2.126 +  def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
   2.127 +  def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
   2.128 +  def is_symbolic(sym: Symbol): Boolean =
   2.129      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
   2.130  
   2.131  
   2.132    /* control symbols */
   2.133  
   2.134 -  def is_ctrl(sym: String): Boolean =
   2.135 +  def is_ctrl(sym: Symbol): Boolean =
   2.136      sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
   2.137  
   2.138 -  def is_controllable(sym: String): Boolean =
   2.139 +  def is_controllable(sym: Symbol): Boolean =
   2.140      !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
   2.141  
   2.142 -  def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
   2.143 -  def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
   2.144 -  def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
   2.145 -  def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
   2.146 -  def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
   2.147 -  def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
   2.148 -  def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
   2.149 +  def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
   2.150 +  def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
   2.151 +  def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
   2.152 +  def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
   2.153 +  def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
   2.154 +  def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
   2.155 +  def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
   2.156  }