1.1 --- a/src/Pure/General/symbol.scala Thu Jul 07 13:48:30 2011 +0200
1.2 +++ b/src/Pure/General/symbol.scala Thu Jul 07 14:10:50 2011 +0200
1.3 @@ -13,6 +13,9 @@
1.4
1.5 object Symbol
1.6 {
1.7 + type Symbol = String
1.8 +
1.9 +
1.10 /* spaces */
1.11
1.12 val spc = ' '
1.13 @@ -64,10 +67,10 @@
1.14
1.15 def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
1.16
1.17 - def is_physical_newline(s: String): Boolean =
1.18 + def is_physical_newline(s: Symbol): Boolean =
1.19 s == "\n" || s == "\r" || s == "\r\n"
1.20
1.21 - def is_malformed(s: String): Boolean =
1.22 + def is_malformed(s: Symbol): Boolean =
1.23 !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
1.24
1.25 class Matcher(text: CharSequence)
1.26 @@ -87,11 +90,11 @@
1.27
1.28 /* iterator */
1.29
1.30 - private val char_symbols: Array[String] =
1.31 + private val char_symbols: Array[Symbol] =
1.32 (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
1.33
1.34 - def iterator(text: CharSequence): Iterator[String] =
1.35 - new Iterator[String]
1.36 + def iterator(text: CharSequence): Iterator[Symbol] =
1.37 + new Iterator[Symbol]
1.38 {
1.39 private val matcher = new Matcher(text)
1.40 private var i = 0
1.41 @@ -216,7 +219,7 @@
1.42 private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
1.43 private val key = new Regex("""(?xs) (.+): """)
1.44
1.45 - private def read_decl(decl: String): (String, Map[String, String]) =
1.46 + private def read_decl(decl: String): (Symbol, Map[String, String]) =
1.47 {
1.48 def err() = error("Bad symbol declaration: " + decl)
1.49
1.50 @@ -235,7 +238,7 @@
1.51 }
1.52 }
1.53
1.54 - private val symbols: List[(String, Map[String, String])] =
1.55 + private val symbols: List[(Symbol, Map[String, String])] =
1.56 Map((
1.57 for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
1.58 yield read_decl(decl)): _*) toList
1.59 @@ -243,13 +246,13 @@
1.60
1.61 /* misc properties */
1.62
1.63 - val names: Map[String, String] =
1.64 + val names: Map[Symbol, String] =
1.65 {
1.66 val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
1.67 Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
1.68 }
1.69
1.70 - val abbrevs: Map[String, String] =
1.71 + val abbrevs: Map[Symbol, String] =
1.72 Map((
1.73 for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
1.74 yield (sym -> props("abbrev"))): _*)
1.75 @@ -295,7 +298,7 @@
1.76
1.77 /* user fonts */
1.78
1.79 - val fonts: Map[String, String] =
1.80 + val fonts: Map[Symbol, String] =
1.81 recode_map((
1.82 for ((sym, props) <- symbols if props.isDefinedAt("font"))
1.83 yield (sym -> props("font"))): _*)
1.84 @@ -350,7 +353,7 @@
1.85
1.86 /* control symbols */
1.87
1.88 - val ctrl_decoded: Set[String] =
1.89 + val ctrl_decoded: Set[Symbol] =
1.90 Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
1.91
1.92 val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
1.93 @@ -366,43 +369,43 @@
1.94
1.95 /* tables */
1.96
1.97 - def names: Map[String, String] = symbols.names
1.98 - def abbrevs: Map[String, String] = symbols.abbrevs
1.99 + def names: Map[Symbol, String] = symbols.names
1.100 + def abbrevs: Map[Symbol, String] = symbols.abbrevs
1.101
1.102 def decode(text: String): String = symbols.decode(text)
1.103 def encode(text: String): String = symbols.encode(text)
1.104
1.105 - def fonts: Map[String, String] = symbols.fonts
1.106 + def fonts: Map[Symbol, String] = symbols.fonts
1.107 def font_names: List[String] = symbols.font_names
1.108 def font_index: Map[String, Int] = symbols.font_index
1.109 - def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
1.110 + def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
1.111
1.112
1.113 /* classification */
1.114
1.115 - def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
1.116 - def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
1.117 - def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
1.118 - def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
1.119 - def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
1.120 - def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
1.121 - def is_symbolic(sym: String): Boolean =
1.122 + def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
1.123 + def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
1.124 + def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
1.125 + def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
1.126 + def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
1.127 + def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
1.128 + def is_symbolic(sym: Symbol): Boolean =
1.129 sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
1.130
1.131
1.132 /* control symbols */
1.133
1.134 - def is_ctrl(sym: String): Boolean =
1.135 + def is_ctrl(sym: Symbol): Boolean =
1.136 sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
1.137
1.138 - def is_controllable(sym: String): Boolean =
1.139 + def is_controllable(sym: Symbol): Boolean =
1.140 !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
1.141
1.142 - def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
1.143 - def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
1.144 - def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
1.145 - def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
1.146 - def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
1.147 - def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
1.148 - def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
1.149 + def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
1.150 + def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
1.151 + def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
1.152 + def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
1.153 + def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
1.154 + def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
1.155 + def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
1.156 }