author  wenzelm 
Tue, 05 Jul 2011 23:18:14 +0200  
changeset 43675  8252d51d70e2 
parent 43511  d138e7482a1b 
child 43695  5130dfe1b7be 
permissions  rwrr 
27901  1 
/* Title: Pure/General/symbol.scala 
2 
Author: Makarius 

3 

27924  4 
Detecting and recoding Isabelle symbols. 
27901  5 
*/ 
6 

7 
package isabelle 

8 

27918  9 
import scala.io.Source 
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

10 
import scala.collection.mutable 
31522  11 
import scala.util.matching.Regex 
27901  12 

13 

31522  14 
object Symbol 
15 
{ 

36763  16 
/* spaces */ 
17 

36816  18 
val spc = ' ' 
19 
val space = " " 

20 

21 
private val static_spaces = space * 4000 

36763  22 

23 
def spaces(k: Int): String = 

24 
{ 

25 
require(k >= 0) 

26 
if (k < static_spaces.length) static_spaces.substring(0, k) 

36816  27 
else space * k 
36763  28 
} 
29 

30 

43418  31 
/* ASCII characters */ 
32 

33 
def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z'  'a' <= c && c <= 'z' 

34 
def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' 

35 
def is_ascii_quasi(c: Char): Boolean = c == '_'  c == '\'' 

36 

37 
def is_ascii_letdig(c: Char): Boolean = 

38 
is_ascii_letter(c)  is_ascii_digit(c)  is_ascii_quasi(c) 

39 

40 
def is_ascii_identifier(s: String): Boolean = 

41 
s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig) 

42 

43 

33998  44 
/* Symbol regexps */ 
27901  45 

31522  46 
private val plain = new Regex("""(?xs) 
40524
6131d7a78ad3
treat Unicode "replacement character" (i.e. decoding error) is malformed;
wenzelm
parents:
40523
diff
changeset

47 
[^\r\\\ud800\udfff\ufffd]  [\ud800\udbff][\udc00\udfff] """) 
37556
2bf29095d26f
treat alternative newline symbols as in Isabelle/ML;
wenzelm
parents:
36816
diff
changeset

48 

40522  49 
private val physical_newline = new Regex("""(?xs) \n  \r\n  \r """) 
27901  50 

31522  51 
private val symbol = new Regex("""(?xs) 
31545
5f1f0a20af4d
discontinued escaped symbols such as \\<forall>  only one backslash should be used;
wenzelm
parents:
31523
diff
changeset

52 
\\ < (?: 
27924  53 
\^? [AZaz][AZaz09_']*  
54 
\^raw: [\x20\x7e\u0100\uffff && [^.>]]* ) >""") 

55 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

56 
private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" + 
40529  57 
""" [\ud800\udbff\ufffd]  \\<\^? """) 
27924  58 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

59 
val regex_total = 
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

60 
new Regex(plain + "" + physical_newline + "" + symbol + "" + malformed_symbol + " .") 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

61 

34137  62 

63 
/* basic matching */ 

64 

37556
2bf29095d26f
treat alternative newline symbols as in Isabelle/ML;
wenzelm
parents:
36816
diff
changeset

65 
def is_plain(c: Char): Boolean = !(c == '\r'  c == '\\'  '\ud800' <= c && c <= '\udfff') 
34137  66 

43675
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

67 
def is_physical_newline(s: String): Boolean = 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

68 
s == "\n"  s == "\r"  s == "\r\n" 
38877  69 

43675
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

70 
def is_malformed(s: String): Boolean = 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

71 
!(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches 
34137  72 

73 
class Matcher(text: CharSequence) 

74 
{ 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

75 
private val matcher = regex_total.pattern.matcher(text) 
34137  76 
def apply(start: Int, end: Int): Int = 
77 
{ 

78 
require(0 <= start && start < end && end <= text.length) 

34316
f879b649ac4c
clarified Symbol.is_plain/is_wellformed  is_closed was rejecting plain backslashes;
wenzelm
parents:
34193
diff
changeset

79 
if (is_plain(text.charAt(start))) 1 
34138  80 
else { 
34137  81 
matcher.region(start, end).lookingAt 
82 
matcher.group.length 

83 
} 

84 
} 

31522  85 
} 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

86 

fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

87 

43489  88 
/* efficient iterators */ 
33998  89 

43675
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

90 
private val char_symbols: Array[String] = 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

91 
(0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

92 

8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

93 
def iterator(text: CharSequence): Iterator[String] = 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

94 
new Iterator[String] 
40522  95 
{ 
43489  96 
private val matcher = new Matcher(text) 
97 
private var i = 0 

98 
def hasNext = i < text.length 

99 
def next = 

100 
{ 

101 
val n = matcher(i, text.length) 

43675
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

102 
val s = 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

103 
if (n == 0) "" 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

104 
else if (n == 1) { 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

105 
val c = text.charAt(i) 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

106 
if (c < char_symbols.length) char_symbols(c) 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

107 
else text.subSequence(i, i + n).toString 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

108 
} 
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43511
diff
changeset

109 
else text.subSequence(i, i + n).toString 
43489  110 
i += n 
111 
s 

112 
} 

33998  113 
} 
43489  114 

33998  115 

116 
/* decoding offsets */ 

117 

118 
class Index(text: CharSequence) 

31929  119 
{ 
120 
case class Entry(chr: Int, sym: Int) 

121 
val index: Array[Entry] = 

122 
{ 

34137  123 
val matcher = new Matcher(text) 
31929  124 
val buf = new mutable.ArrayBuffer[Entry] 
125 
var chr = 0 

126 
var sym = 0 

33998  127 
while (chr < text.length) { 
34137  128 
val n = matcher(chr, text.length) 
129 
chr += n 

31929  130 
sym += 1 
34137  131 
if (n > 1) buf += Entry(chr, sym) 
31929  132 
} 
133 
buf.toArray 

134 
} 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
37556
diff
changeset

135 
def decode(sym1: Int): Int = 
31929  136 
{ 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
37556
diff
changeset

137 
val sym = sym1  1 
31929  138 
val end = index.length 
139 
def bisect(a: Int, b: Int): Int = 

140 
{ 

141 
if (a < b) { 

142 
val c = (a + b) / 2 

143 
if (sym < index(c).sym) bisect(a, c) 

144 
else if (c + 1 == end  sym < index(c + 1).sym) c 

145 
else bisect(c + 1, b) 

146 
} 

147 
else 1 

148 
} 

149 
val i = bisect(0, end) 

150 
if (i < 0) sym 

151 
else index(i).chr + sym  index(i).sym 

152 
} 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
37556
diff
changeset

153 
def decode(range: Text.Range): Text.Range = range.map(decode(_)) 
31929  154 
} 
155 

156 

33998  157 
/* recoding text */ 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

158 

31522  159 
private class Recoder(list: List[(String, String)]) 
160 
{ 

161 
private val (min, max) = 

162 
{ 

27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

163 
var min = '\uffff' 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

164 
var max = '\u0000' 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

165 
for ((x, _) < list) { 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

166 
val c = x(0) 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

167 
if (c < min) min = c 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

168 
if (c > max) max = c 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

169 
} 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

170 
(min, max) 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

171 
} 
40443  172 
private val table = 
173 
{ 

174 
var tab = Map[String, String]() 

175 
for ((x, y) < list) { 

176 
tab.get(x) match { 

177 
case None => tab += (x > y) 

178 
case Some(z) => 

179 
error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"") 

180 
} 

181 
} 

182 
tab 

183 
} 

31522  184 
def recode(text: String): String = 
185 
{ 

27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

186 
val len = text.length 
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

187 
val matcher = regex_total.pattern.matcher(text) 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

188 
val result = new StringBuilder(len) 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

189 
var i = 0 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

190 
while (i < len) { 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

191 
val c = text(i) 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

192 
if (min <= c && c <= max) { 
31929  193 
matcher.region(i, len).lookingAt 
27938  194 
val x = matcher.group 
31522  195 
result.append(table.get(x) getOrElse x) 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

196 
i = matcher.end 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

197 
} 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

198 
else { result.append(c); i += 1 } 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

199 
} 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

200 
result.toString 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

201 
} 
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

202 
} 
27924  203 

27918  204 

27923
7ebe9d38743a
use scala.collection.jcl.HashMap, which seems to be more efficient;
wenzelm
parents:
27918
diff
changeset

205 

27927  206 
/** Symbol interpretation **/ 
207 

34137  208 
class Interpretation(symbol_decls: List[String]) 
29569
f3f529b5d8fb
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
wenzelm
parents:
29174
diff
changeset

209 
{ 
31522  210 
/* read symbols */ 
211 

212 
private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) 

213 
private val key = new Regex("""(?xs) (.+): """) 

214 

215 
private def read_decl(decl: String): (String, Map[String, String]) = 

216 
{ 

217 
def err() = error("Bad symbol declaration: " + decl) 

218 

219 
def read_props(props: List[String]): Map[String, String] = 

220 
{ 

221 
props match { 

222 
case Nil => Map() 

223 
case _ :: Nil => err() 

224 
case key(x) :: y :: rest => read_props(rest) + (x > y) 

225 
case _ => err() 

226 
} 

227 
} 

228 
decl.split("\\s+").toList match { 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

229 
case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props)) 
34193  230 
case _ => err() 
31522  231 
} 
232 
} 

233 

234 
private val symbols: List[(String, Map[String, String])] = 

40443  235 
Map(( 
236 
for (decl < symbol_decls if !empty.pattern.matcher(decl).matches) 

237 
yield read_decl(decl)): _*) toList 

31522  238 

239 

31651  240 
/* misc properties */ 
241 

34134  242 
val names: Map[String, String] = 
243 
{ 

43456
8a6de1a6e1dc
names for control symbols without "^", which is relevant for completion;
wenzelm
parents:
43455
diff
changeset

244 
val name = new Regex("""\\<\^?([AZaz][AZaz09_']*)>""") 
31651  245 
Map((for ((sym @ name(a), _) < symbols) yield (sym > a)): _*) 
246 
} 

247 

43488  248 
val abbrevs: Map[String, String] = 
249 
Map(( 

250 
for ((sym, props) < symbols if props.isDefinedAt("abbrev")) 

251 
yield (sym > props("abbrev"))): _*) 

252 

253 

43490  254 
/* recoding */ 
31522  255 

256 
private val (decoder, encoder) = 

257 
{ 

258 
val mapping = 

259 
for { 

260 
(sym, props) < symbols 

261 
val code = 

262 
try { Integer.decode(props("code")).intValue } 

263 
catch { 

264 
case _: NoSuchElementException => error("Missing code for symbol " + sym) 

265 
case _: NumberFormatException => error("Bad code for symbol " + sym) 

266 
} 

267 
val ch = new String(Character.toChars(code)) 

34193  268 
} yield { 
269 
if (code < 128) error("Illegal ASCII code for symbol " + sym) 

270 
else (sym, ch) 

271 
} 

31545
5f1f0a20af4d
discontinued escaped symbols such as \\<forall>  only one backslash should be used;
wenzelm
parents:
31523
diff
changeset

272 
(new Recoder(mapping), 
31548  273 
new Recoder(mapping map { case (x, y) => (y, x) })) 
31522  274 
} 
27918  275 

34098  276 
def decode(text: String): String = decoder.recode(text) 
277 
def encode(text: String): String = encoder.recode(text) 

34134  278 

43490  279 
private def recode_set(elems: String*): Set[String] = 
280 
{ 

281 
val content = elems.toList 

282 
Set((content ::: content.map(decode)): _*) 

283 
} 

284 

285 
private def recode_map[A](elems: (String, A)*): Map[String, A] = 

286 
{ 

287 
val content = elems.toList 

288 
Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*) 

289 
} 

290 

291 

292 
/* user fonts */ 

293 

294 
val fonts: Map[String, String] = 

295 
recode_map(( 

296 
for ((sym, props) < symbols if props.isDefinedAt("font")) 

297 
yield (sym > props("font"))): _*) 

298 

299 
val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList 

300 
val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*) 

301 

302 
def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_)) 

303 

34134  304 

305 
/* classification */ 

306 

43490  307 
private val letters = recode_set( 
34134  308 
"A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", 
309 
"N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", 

310 
"a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", 

311 
"n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", 

312 

313 
"\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>", 

314 
"\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>", 

315 
"\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>", 

316 
"\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>", 

317 
"\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>", 

318 
"\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>", 

319 
"\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>", 

320 
"\\<x>", "\\<y>", "\\<z>", 

321 

322 
"\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>", 

323 
"\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>", 

324 
"\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>", 

325 
"\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>", 

326 
"\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>", 

327 
"\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>", 

328 
"\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>", 

329 
"\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>", 

330 
"\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>", 

331 

332 
"\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>", 

333 
"\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>", 

334 
"\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>", 

335 
"\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>", 

336 
"\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>", 

337 
"\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>", 

338 
"\\<Psi>", "\\<Omega>", 

339 

340 
"\\<^isub>", "\\<^isup>") 

341 

34138  342 
private val blanks = 
43490  343 
recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>") 
34138  344 

345 
private val sym_chars = 

346 
Set("!", "#", "$", "%", "&", "*", "+", "", "/", "<", "=", ">", "?", "@", "^", "_", "", "~") 

34134  347 

348 
def is_letter(sym: String): Boolean = letters.contains(sym) 

34138  349 
def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' 
34134  350 
def is_quasi(sym: String): Boolean = sym == "_"  sym == "'" 
34138  351 
def is_letdig(sym: String): Boolean = is_letter(sym)  is_digit(sym)  is_quasi(sym) 
34134  352 
def is_blank(sym: String): Boolean = blanks.contains(sym) 
34138  353 
def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym) 
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

354 
def is_symbolic(sym: String): Boolean = 
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40522
diff
changeset

355 
sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^") 
43455  356 

357 

43488  358 
/* control symbols */ 
359 

360 
private val ctrl_decoded: Set[String] = 

361 
Set((for ((sym, _) < symbols if sym.startsWith("\\<^")) yield decode(sym)): _*) 

362 

363 
def is_ctrl(sym: String): Boolean = 

364 
sym.startsWith("\\<^")  ctrl_decoded.contains(sym) 

43455  365 

43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43418
diff
changeset

366 
def is_controllable(sym: String): Boolean = 
43488  367 
!is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym) 
43455  368 

369 
private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>")) 

370 
private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>")) 

371 
def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym) 

372 
def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym) 

43511  373 

374 
val bold_decoded = decode("\\<^bold>") 

375 
val bsub_decoded = decode("\\<^bsub>") 

376 
val esub_decoded = decode("\\<^esub>") 

377 
val bsup_decoded = decode("\\<^bsup>") 

378 
val esup_decoded = decode("\\<^esup>") 

27918  379 
} 
27901  380 
} 