author  wenzelm 
Sat, 19 Dec 2015 15:14:59 +0100  
changeset 61865  6dcc9e4f1aa6 
parent 61579  634cd44bb1d3 
child 61959  364007370bb7 
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 

55618  9 

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 
48922  12 
import scala.annotation.tailrec 
27901  13 

14 

31522  15 
object Symbol 
16 
{ 

43696  17 
type Symbol = String 
18 

55884
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

19 
// counting Isabelle symbols, starting from 1 
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

20 
type Offset = Text.Offset 
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

21 
type Range = Text.Range 
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

22 

43696  23 

61865  24 
/* spaces */ 
25 

26 
val space = " " 

27 

28 
private val static_spaces = space * 4000 

29 

30 
def spaces(n: Int): String = 

31 
{ 

32 
require(n >= 0) 

33 
if (n < static_spaces.length) static_spaces.substring(0, n) 

34 
else space * n 

35 
} 

36 

37 

43418  38 
/* ASCII characters */ 
39 

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

55497  41 

43418  42 
def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' 
55497  43 

44 
def is_ascii_hex(c: Char): Boolean = 

45 
'0' <= c && c <= '9'  'A' <= c && c <= 'F'  'a' <= c && c <= 'f' 

46 

43418  47 
def is_ascii_quasi(c: Char): Boolean = c == '_'  c == '\'' 
48 

55497  49 
def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c) 
50 

43418  51 
def is_ascii_letdig(c: Char): Boolean = 
52 
is_ascii_letter(c)  is_ascii_digit(c)  is_ascii_quasi(c) 

53 

54 
def is_ascii_identifier(s: String): Boolean = 

50238
98d35a7368bd
more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents:
50233
diff
changeset

55 
s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) 
43418  56 

57 

48775  58 
/* symbol matching */ 
27901  59 

48775  60 
private val symbol_total = new Regex("""(?xs) 
61 
[\ud800\udbff][\udc00\udfff]  \r\n  

62 
\\ < (?: \^raw: [\x20\x7e\u0100\uffff && [^.>]]*  \^? ([AZaz][AZaz09_']*)? ) >?  

63 
.""") 

27924  64 

48775  65 
private def is_plain(c: Char): Boolean = 
66 
!(c == '\r'  c == '\\'  Character.isHighSurrogate(c)) 

48773
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

67 

0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

68 
def is_malformed(s: Symbol): Boolean = 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

69 
s.length match { 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

70 
case 1 => 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

71 
val c = s(0) 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

72 
Character.isHighSurrogate(c)  Character.isLowSurrogate(c)  c == '\ufffd' 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

73 
case 2 => 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

74 
val c1 = s(0) 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

75 
val c2 = s(1) 
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

76 
!(c1 == '\r' && c2 == '\n'  Character.isSurrogatePair(c1, c2)) 
48774  77 
case _ => !s.endsWith(">")  s == "\\<>"  s == "\\<^>" 
48773
0e1bab274672
more liberal scanning of potentially malformed symbols;
wenzelm
parents:
48704
diff
changeset

78 
} 
34137  79 

54734
b91afc3aa3e6
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
wenzelm
parents:
53400
diff
changeset

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

81 
s == "\n"  s == "\r"  s == "\r\n" 
38877  82 

34137  83 
class Matcher(text: CharSequence) 
84 
{ 

48775  85 
private val matcher = symbol_total.pattern.matcher(text) 
34137  86 
def apply(start: Int, end: Int): Int = 
87 
{ 

88 
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

89 
if (is_plain(text.charAt(start))) 1 
34138  90 
else { 
34137  91 
matcher.region(start, end).lookingAt 
92 
matcher.group.length 

93 
} 

94 
} 

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

96 

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

97 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

98 
/* iterator */ 
33998  99 

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

101 
(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

102 

43696  103 
def iterator(text: CharSequence): Iterator[Symbol] = 
104 
new Iterator[Symbol] 

40522  105 
{ 
43489  106 
private val matcher = new Matcher(text) 
107 
private var i = 0 

108 
def hasNext = i < text.length 

109 
def next = 

110 
{ 

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

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

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

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

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

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

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

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

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

119 
else text.subSequence(i, i + n).toString 
43489  120 
i += n 
121 
s 

122 
} 

33998  123 
} 
43489  124 

44949  125 
def explode(text: CharSequence): List[Symbol] = iterator(text).toList 
126 

48922  127 
def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) = 
128 
{ 

129 
var (line, column) = pos 

130 
for (sym < iterator(text)) { 

54734
b91afc3aa3e6
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
wenzelm
parents:
53400
diff
changeset

131 
if (is_newline(sym)) { line += 1; column = 1 } 
48922  132 
else column += 1 
133 
} 

134 
(line, column) 

135 
} 

136 

33998  137 

138 
/* decoding offsets */ 

139 

52507  140 
object Index 
141 
{ 

56471
2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

142 
private sealed case class Entry(chr: Int, sym: Int) 
52507  143 

56472  144 
val empty: Index = new Index(Nil) 
56471
2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

145 

2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

146 
def apply(text: CharSequence): Index = 
31929  147 
{ 
34137  148 
val matcher = new Matcher(text) 
56471
2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

149 
val buf = new mutable.ListBuffer[Entry] 
31929  150 
var chr = 0 
151 
var sym = 0 

33998  152 
while (chr < text.length) { 
34137  153 
val n = matcher(chr, text.length) 
154 
chr += n 

31929  155 
sym += 1 
34137  156 
if (n > 1) buf += Entry(chr, sym) 
31929  157 
} 
56472  158 
if (buf.isEmpty) empty else new Index(buf.toList) 
31929  159 
} 
56471
2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

160 
} 
55430  161 

56472  162 
final class Index private(entries: List[Index.Entry]) 
56471
2293a4350716
more frugal Symbol.Index  no need to waste space on mostly empty arrays;
wenzelm
parents:
56338
diff
changeset

163 
{ 
56472  164 
private val hash: Int = entries.hashCode 
165 
private val index: Array[Index.Entry] = entries.toArray 

166 

55884
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

167 
def decode(symbol_offset: Offset): Text.Offset = 
31929  168 
{ 
55884
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

169 
val sym = symbol_offset  1 
31929  170 
val end = index.length 
48922  171 
@tailrec def bisect(a: Int, b: Int): Int = 
31929  172 
{ 
173 
if (a < b) { 

174 
val c = (a + b) / 2 

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

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

177 
else bisect(c + 1, b) 

178 
} 

179 
else 1 

180 
} 

181 
val i = bisect(0, end) 

182 
if (i < 0) sym 

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

184 
} 

55884
f2c0eaedd579
tuned signature  emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55618
diff
changeset

185 
def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_)) 
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

186 

56338
f968f4e3d520
proper structural hashCode, which is required for Command.File equals (NB: Array has physical object identity);
wenzelm
parents:
56335
diff
changeset

187 
override def hashCode: Int = hash 
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

188 
override def equals(that: Any): Boolean = 
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

189 
that match { 
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

190 
case other: Index => index.sameElements(other.index) 
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

191 
case _ => false 
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
55884
diff
changeset

192 
} 
31929  193 
} 
194 

195 

56746  196 
/* text chunks */ 
197 

198 
object Text_Chunk 

199 
{ 

200 
sealed abstract class Name 

201 
case object Default extends Name 

202 
case class Id(id: Document_ID.Generic) extends Name 

203 
case class File(name: String) extends Name 

204 

205 
def apply(text: CharSequence): Text_Chunk = 

206 
new Text_Chunk(Text.Range(0, text.length), Index(text)) 

207 
} 

208 

209 
final class Text_Chunk private(val range: Text.Range, private val index: Index) 

210 
{ 

211 
override def hashCode: Int = (range, index).hashCode 

212 
override def equals(that: Any): Boolean = 

213 
that match { 

214 
case other: Text_Chunk => 

215 
range == other.range && 

216 
index == other.index 

217 
case _ => false 

218 
} 

219 

57840  220 
override def toString: String = "Text_Chunk" + range.toString 
221 

56746  222 
def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset) 
223 
def decode(symbol_range: Range): Text.Range = index.decode(symbol_range) 

224 
def incorporate(symbol_range: Range): Option[Text.Range] = 

225 
{ 

226 
def in(r: Range): Option[Text.Range] = 

227 
range.try_restrict(decode(r)) match { 

228 
case Some(r1) if !r1.is_singularity => Some(r1) 

229 
case _ => None 

230 
} 

231 
in(symbol_range) orElse in(symbol_range  1) 

232 
} 

233 
} 

234 

235 

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

237 

31522  238 
private class Recoder(list: List[(String, String)]) 
239 
{ 

240 
private val (min, max) = 

241 
{ 

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

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

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

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

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

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

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

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

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

250 
} 
40443  251 
private val table = 
252 
{ 

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

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

255 
tab.get(x) match { 

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

257 
case Some(z) => 

44181  258 
error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) 
40443  259 
} 
260 
} 

261 
tab 

262 
} 

31522  263 
def recode(text: String): String = 
264 
{ 

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

265 
val len = text.length 
48775  266 
val matcher = symbol_total.pattern.matcher(text) 
27937
fdf77e7be01a
more robust pattern: look at longer matches first, added catchall case;
wenzelm
parents:
27935
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

281 
} 
27924  282 

27918  283 

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

284 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

285 
/** symbol interpretation **/ 
27927  286 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

287 
private lazy val symbols = 
50564
c6fde2fc4217
allow to suppress ISABELLE_SYMBOLS for experiments;
wenzelm
parents:
50291
diff
changeset

288 
new Interpretation(File.try_read(Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")))) 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

289 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

290 
private class Interpretation(symbols_spec: String) 
29569
f3f529b5d8fb
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
wenzelm
parents:
29174
diff
changeset

291 
{ 
31522  292 
/* read symbols */ 
293 

50136
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

294 
private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

295 
private val Key = new Regex("""(?xs) (.+): """) 
31522  296 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

297 
private def read_decl(decl: String): (Symbol, Properties.T) = 
31522  298 
{ 
299 
def err() = error("Bad symbol declaration: " + decl) 

300 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

301 
def read_props(props: List[String]): Properties.T = 
31522  302 
{ 
303 
props match { 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

304 
case Nil => Nil 
31522  305 
case _ :: Nil => err() 
61174  306 
case Key(x) :: y :: rest => (x > y.replace('\u2423', ' ')) :: read_props(rest) 
31522  307 
case _ => err() 
308 
} 

309 
} 

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

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

311 
case sym :: props if sym.length > 1 && !is_malformed(sym) => 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

312 
(sym, read_props(props)) 
34193  313 
case _ => err() 
31522  314 
} 
315 
} 

316 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

317 
private val symbols: List[(Symbol, Properties.T)] = 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

318 
(((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /: 
50136
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

319 
split_lines(symbols_spec).reverse) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

320 
{ case (res, No_Decl()) => res 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

321 
case ((list, known), decl) => 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

322 
val (sym, props) = read_decl(decl) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

323 
if (known(sym)) (list, known) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

324 
else ((sym, props) :: list, known + sym) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

325 
})._1 
31522  326 

327 

53400  328 
/* basic properties */ 
329 

330 
val properties: Map[Symbol, Properties.T] = Map(symbols: _*) 

31651  331 

43696  332 
val names: Map[Symbol, String] = 
34134  333 
{ 
43456
8a6de1a6e1dc
names for control symbols without "^", which is relevant for completion;
wenzelm
parents:
43455
diff
changeset

334 
val name = new Regex("""\\<\^?([AZaz][AZaz09_']*)>""") 
60215  335 
Map((for ((sym @ name(a), _) < symbols) yield sym > a): _*) 
31651  336 
} 
337 

50136
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

338 
val groups: List[(String, List[Symbol])] = 
53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

339 
symbols.map({ case (sym, props) => 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

340 
val gs = for (("group", g) < props) yield g 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

341 
if (gs.isEmpty) List(sym > "unsorted") else gs.map(sym > _) 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

342 
}).flatten 
50136
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

343 
.groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) }) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

344 
.sortBy(_._1) 
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

345 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

346 
val abbrevs: Multi_Map[Symbol, String] = 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

347 
Multi_Map(( 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

348 
for { 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

349 
(sym, props) < symbols 
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

350 
("abbrev", a) < props.reverse 
60215  351 
} yield sym > a): _*) 
43488  352 

61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

353 
val codes: List[(String, Int)] = 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

354 
{ 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

355 
val Code = new Properties.String("code") 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

356 
for { 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

357 
(sym, props) < symbols 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

358 
code = 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

359 
props match { 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

360 
case Code(s) => 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

361 
try { Integer.decode(s).intValue } 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

362 
catch { case _: NumberFormatException => error("Bad code for symbol " + sym) } 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

363 
case _ => error("Missing code for symbol " + sym) 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

364 
} 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

365 
} yield { 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

366 
if (code < 128) error("Illegal ASCII code for symbol " + sym) 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

367 
else (sym, code) 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

368 
} 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

369 
} 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

370 

43488  371 

43490  372 
/* recoding */ 
31522  373 

374 
private val (decoder, encoder) = 

375 
{ 

376 
val mapping = 

61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

377 
for ((sym, code) < codes) yield (sym, new String(Character.toChars(code))) 
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

378 
(new Recoder(mapping), new Recoder(for ((x, y) < mapping) yield (y, x))) 
31522  379 
} 
27918  380 

34098  381 
def decode(text: String): String = decoder.recode(text) 
382 
def encode(text: String): String = encoder.recode(text) 

34134  383 

43490  384 
private def recode_set(elems: String*): Set[String] = 
385 
{ 

386 
val content = elems.toList 

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

388 
} 

389 

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

391 
{ 

392 
val content = elems.toList 

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

394 
} 

395 

396 

397 
/* user fonts */ 

398 

53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

399 
private val Font = new Properties.String("font") 
43696  400 
val fonts: Map[Symbol, String] = 
60215  401 
recode_map((for ((sym, Font(font)) < symbols) yield sym > font): _*) 
43490  402 

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

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

405 

34134  406 

407 
/* classification */ 

408 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

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

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

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

414 

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

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

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

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

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

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

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

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

423 

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

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

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

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

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

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

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

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

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

433 

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

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

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

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

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

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

52616
3ac2878764f9
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
wenzelm
parents:
52507
diff
changeset

440 
"\\<Psi>", "\\<Omega>") 
34134  441 

61865  442 
val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n") 
34138  443 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

444 
val sym_chars = 
34138  445 
Set("!", "#", "$", "%", "&", "*", "+", "", "/", "<", "=", ">", "?", "@", "^", "_", "", "~") 
34134  446 

44992
aa34d2d049ce
refined Symbol.is_symbolic  cover recoded versions as well;
wenzelm
parents:
44949
diff
changeset

447 
val symbolic = recode_set((for { (sym, _) < symbols; if raw_symbolic(sym) } yield sym): _*) 
aa34d2d049ce
refined Symbol.is_symbolic  cover recoded versions as well;
wenzelm
parents:
44949
diff
changeset

448 

43455  449 

61579  450 
/* comment */ 
451 

452 
val comment_decoded = decode(comment) 

453 

454 

55033  455 
/* cartouches */ 
456 

457 
val open_decoded = decode(open) 

458 
val close_decoded = decode(close) 

459 

460 

43488  461 
/* control symbols */ 
462 

59107  463 
val control_decoded: Set[Symbol] = 
43488  464 
Set((for ((sym, _) < symbols if sym.startsWith("\\<^")) yield decode(sym)): _*) 
465 

44238
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

466 
val sub_decoded = decode("\\<^sub>") 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

467 
val sup_decoded = decode("\\<^sup>") 
43511  468 
val bsub_decoded = decode("\\<^bsub>") 
469 
val esub_decoded = decode("\\<^esub>") 

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

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

44238
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

472 
val bold_decoded = decode("\\<^bold>") 
61483  473 
val emph_decoded = decode("\\<^emph>") 
27918  474 
} 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

475 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

476 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

477 
/* tables */ 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

478 

53400  479 
def properties: Map[Symbol, Properties.T] = symbols.properties 
43696  480 
def names: Map[Symbol, String] = symbols.names 
50136
a96bd08258a2
support for symbol groups, retaining original order of declarations;
wenzelm
parents:
48922
diff
changeset

481 
def groups: List[(String, List[Symbol])] = symbols.groups 
53316
c3e549e0d3c7
allow multiple symbol properties, notably groups and abbrevs;
wenzelm
parents:
53021
diff
changeset

482 
def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs 
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61174
diff
changeset

483 
def codes: List[(String, Int)] = symbols.codes 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

484 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

485 
def decode(text: String): String = symbols.decode(text) 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

486 
def encode(text: String): String = symbols.encode(text) 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

487 

53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53316
diff
changeset

488 
def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x))) 
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53316
diff
changeset

489 
def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x))) 
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53316
diff
changeset

490 

50291
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

491 
def decode_strict(text: String): String = 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

492 
{ 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

493 
val decoded = decode(text) 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

494 
if (encode(decoded) == text) decoded 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

495 
else { 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

496 
val bad = new mutable.ListBuffer[Symbol] 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

497 
for (s < iterator(text) if encode(decode(s)) != s && !bad.contains(s)) 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

498 
bad += s 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

499 
error("Bad Unicode symbols in text: " + commas_quote(bad)) 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

500 
} 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

501 
} 
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50238
diff
changeset

502 

43696  503 
def fonts: Map[Symbol, String] = symbols.fonts 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

504 
def font_names: List[String] = symbols.font_names 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

505 
def font_index: Map[String, Int] = symbols.font_index 
43696  506 
def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_)) 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

507 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

508 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

509 
/* classification */ 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

510 

43696  511 
def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym) 
512 
def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' 

513 
def is_quasi(sym: Symbol): Boolean = sym == "_"  sym == "'" 

514 
def is_letdig(sym: Symbol): Boolean = is_letter(sym)  is_digit(sym)  is_quasi(sym) 

515 
def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym) 

44992
aa34d2d049ce
refined Symbol.is_symbolic  cover recoded versions as well;
wenzelm
parents:
44949
diff
changeset

516 

55033  517 

61579  518 
/* comment */ 
519 

520 
val comment: Symbol = "\\<comment>" 

521 
def comment_decoded: Symbol = symbols.comment_decoded 

522 

523 

55033  524 
/* cartouches */ 
525 

61579  526 
val open: Symbol = "\\<open>" 
527 
val close: Symbol = "\\<close>" 

55033  528 

529 
def open_decoded: Symbol = symbols.open_decoded 

530 
def close_decoded: Symbol = symbols.close_decoded 

531 

532 
def is_open(sym: Symbol): Boolean = sym == open_decoded  sym == open 

533 
def is_close(sym: Symbol): Boolean = sym == close_decoded  sym == close 

534 

535 

536 
/* symbols for symbolic identifiers */ 

44992
aa34d2d049ce
refined Symbol.is_symbolic  cover recoded versions as well;
wenzelm
parents:
44949
diff
changeset

537 

aa34d2d049ce
refined Symbol.is_symbolic  cover recoded versions as well;
wenzelm
parents:
44949
diff
changeset

538 
private def raw_symbolic(sym: Symbol): Boolean = 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

539 
sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^") 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

540 

55033  541 
def is_symbolic(sym: Symbol): Boolean = 
542 
!is_open(sym) && !is_close(sym) && (raw_symbolic(sym)  symbols.symbolic.contains(sym)) 

543 

544 
def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym) 

545 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

546 

5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

547 
/* control symbols */ 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

548 

59107  549 
def is_control(sym: Symbol): Boolean = 
61470  550 
(sym.startsWith("\\<^") && sym.endsWith(">"))  symbols.control_decoded.contains(sym) 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

551 

43696  552 
def is_controllable(sym: Symbol): Boolean = 
59107  553 
!is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym) 
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43675
diff
changeset

554 

44238
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

555 
def sub_decoded: Symbol = symbols.sub_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

556 
def sup_decoded: Symbol = symbols.sup_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

557 
def bsub_decoded: Symbol = symbols.bsub_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

558 
def esub_decoded: Symbol = symbols.esub_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

559 
def bsup_decoded: Symbol = symbols.bsup_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

560 
def esup_decoded: Symbol = symbols.esup_decoded 
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44181
diff
changeset

561 
def bold_decoded: Symbol = symbols.bold_decoded 
61483  562 
def emph_decoded: Symbol = symbols.emph_decoded 
27901  563 
} 