--- 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 =>
--- 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
}