# HG changeset patch
# User wenzelm
# Date 1310040650 -7200
# Node ID 58bb7ca5c7a2972b95380bf64895645adeb65e6d
# Parent  5130dfe1b7beafe187ca4c9c050b02e5b572fa58
explicit indication of type Symbol.Symbol;

diff -r 5130dfe1b7be -r 58bb7ca5c7a2 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Jul 07 13:48:30 2011 +0200
+++ b/src/Pure/General/scan.scala	Thu Jul 07 14:10:50 2011 +0200
@@ -161,7 +161,7 @@
 
     /* symbol range */
 
-    def symbol_range(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
+    def symbol_range(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
       new Parser[String]
       {
         def apply(in: Input) =
@@ -187,25 +187,30 @@
         }
       }.named("symbol_range")
 
-    def one(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, 1)
-    def many(pred: String => Boolean): Parser[String] = symbol_range(pred, 0, Integer.MAX_VALUE)
-    def many1(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, Integer.MAX_VALUE)
+    def one(pred: Symbol.Symbol => Boolean): Parser[String] =
+      symbol_range(pred, 1, 1)
+
+    def many(pred: Symbol.Symbol => Boolean): Parser[String] =
+      symbol_range(pred, 0, Integer.MAX_VALUE)
+
+    def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
+      symbol_range(pred, 1, Integer.MAX_VALUE)
 
 
     /* quoted strings */
 
-    private def quoted_body(quote: String): Parser[String] =
+    private def quoted_body(quote: Symbol.Symbol): Parser[String] =
     {
       rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
         (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
     }
 
-    private def quoted(quote: String): Parser[String] =
+    private def quoted(quote: Symbol.Symbol): Parser[String] =
     {
       quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
     }.named("quoted")
 
-    def quoted_content(quote: String, source: String): String =
+    def quoted_content(quote: Symbol.Symbol, source: String): String =
     {
       require(parseAll(quoted(quote), source).successful)
       val body = source.substring(1, source.length - 1)
@@ -218,7 +223,7 @@
       else body
     }
 
-    def quoted_context(quote: String, ctxt: Context): Parser[(String, Context)] =
+    def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] =
     {
       ctxt match {
         case Finished =>
diff -r 5130dfe1b7be -r 58bb7ca5c7a2 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Jul 07 13:48:30 2011 +0200
+++ b/src/Pure/General/symbol.scala	Thu Jul 07 14:10:50 2011 +0200
@@ -13,6 +13,9 @@
 
 object Symbol
 {
+  type Symbol = String
+
+
   /* spaces */
 
   val spc = ' '
@@ -64,10 +67,10 @@
 
   def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
-  def is_physical_newline(s: String): Boolean =
+  def is_physical_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
-  def is_malformed(s: String): Boolean =
+  def is_malformed(s: Symbol): Boolean =
     !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
 
   class Matcher(text: CharSequence)
@@ -87,11 +90,11 @@
 
   /* iterator */
 
-  private val char_symbols: Array[String] =
+  private val char_symbols: Array[Symbol] =
     (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
 
-  def iterator(text: CharSequence): Iterator[String] =
-    new Iterator[String]
+  def iterator(text: CharSequence): Iterator[Symbol] =
+    new Iterator[Symbol]
     {
       private val matcher = new Matcher(text)
       private var i = 0
@@ -216,7 +219,7 @@
     private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
     private val key = new Regex("""(?xs) (.+): """)
 
-    private def read_decl(decl: String): (String, Map[String, String]) =
+    private def read_decl(decl: String): (Symbol, Map[String, String]) =
     {
       def err() = error("Bad symbol declaration: " + decl)
 
@@ -235,7 +238,7 @@
       }
     }
 
-    private val symbols: List[(String, Map[String, String])] =
+    private val symbols: List[(Symbol, Map[String, String])] =
       Map((
         for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
           yield read_decl(decl)): _*) toList
@@ -243,13 +246,13 @@
 
     /* misc properties */
 
-    val names: Map[String, String] =
+    val names: Map[Symbol, String] =
     {
       val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
-    val abbrevs: Map[String, String] =
+    val abbrevs: Map[Symbol, String] =
       Map((
         for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
           yield (sym -> props("abbrev"))): _*)
@@ -295,7 +298,7 @@
 
     /* user fonts */
 
-    val fonts: Map[String, String] =
+    val fonts: Map[Symbol, String] =
       recode_map((
         for ((sym, props) <- symbols if props.isDefinedAt("font"))
           yield (sym -> props("font"))): _*)
@@ -350,7 +353,7 @@
 
     /* control symbols */
 
-    val ctrl_decoded: Set[String] =
+    val ctrl_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
     val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
@@ -366,43 +369,43 @@
 
   /* tables */
 
-  def names: Map[String, String] = symbols.names
-  def abbrevs: Map[String, String] = symbols.abbrevs
+  def names: Map[Symbol, String] = symbols.names
+  def abbrevs: Map[Symbol, 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 fonts: Map[Symbol, 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(_))
+  def lookup_font(sym: Symbol): 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 =
+  def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
+  def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
+  def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
+  def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
+  def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
+  def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
+  def is_symbolic(sym: Symbol): Boolean =
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
 
   /* control symbols */
 
-  def is_ctrl(sym: String): Boolean =
+  def is_ctrl(sym: Symbol): Boolean =
     sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
 
-  def is_controllable(sym: String): Boolean =
+  def is_controllable(sym: Symbol): 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
+  def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
+  def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
+  def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
+  def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
+  def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
+  def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
+  def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
 }