14 import javax.swing.text.Segment |
14 import javax.swing.text.Segment |
15 |
15 |
16 |
16 |
17 object Token_Markup |
17 object Token_Markup |
18 { |
18 { |
19 /* extended jEdit syntax styles */ |
19 /* extended syntax styles */ |
20 |
20 |
21 private val plain_range: Int = JEditToken.ID_COUNT |
21 private val plain_range: Int = JEditToken.ID_COUNT |
22 private def check_range(i: Int) { require(0 <= i && i < plain_range) } |
22 private def check_range(i: Int) { require(0 <= i && i < plain_range) } |
23 |
23 |
24 def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } |
24 def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } |
25 def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } |
25 def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } |
26 val hidden: Byte = (3 * plain_range).toByte |
26 val hidden: Byte = (3 * plain_range).toByte |
|
27 |
|
28 // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup> |
|
29 // FIXME \\<^bold> \\<^loc> |
|
30 |
|
31 private val ctrl_styles: Map[String, Byte => Byte] = |
|
32 Map( |
|
33 "\\<^sub>" -> subscript, |
|
34 "\\<^sup>" -> superscript, |
|
35 "\\<^isub>" -> subscript, |
|
36 "\\<^isup>" -> superscript) |
|
37 |
|
38 private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence) |
|
39 : Map[Text.Offset, Byte => Byte] = |
|
40 { |
|
41 if (Isabelle.extended_styles) { |
|
42 var result = Map[Text.Offset, Byte => Byte]() |
|
43 def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) |
|
44 { |
|
45 for (i <- start until stop) result += (i -> style) |
|
46 } |
|
47 var offset = 0 |
|
48 var ctrl = "" |
|
49 for (sym <- Symbol.iterator(text).map(_.toString)) { |
|
50 if (ctrl_styles.isDefinedAt(sym)) ctrl = sym |
|
51 else if (ctrl != "") { |
|
52 if (symbols.is_controllable(sym)) { |
|
53 mark(offset - ctrl.length, offset, _ => hidden) |
|
54 mark(offset, offset + sym.length, ctrl_styles(ctrl)) |
|
55 } |
|
56 ctrl = "" |
|
57 } |
|
58 offset += sym.length |
|
59 } |
|
60 result |
|
61 } |
|
62 else Map.empty |
|
63 } |
27 |
64 |
28 |
65 |
29 /* token marker */ |
66 /* token marker */ |
30 |
67 |
31 private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") |
68 private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") |
53 case _ => Scan.Finished |
90 case _ => Scan.Finished |
54 } |
91 } |
55 val (tokens, ctxt1) = syntax.scan_context(line, ctxt) |
92 val (tokens, ctxt1) = syntax.scan_context(line, ctxt) |
56 val context1 = new Line_Context(ctxt1) |
93 val context1 = new Line_Context(ctxt1) |
57 |
94 |
|
95 val extended = extended_styles(session.system.symbols, line) |
|
96 |
58 var offset = 0 |
97 var offset = 0 |
59 for (token <- tokens) { |
98 for (token <- tokens) { |
60 val style = Isabelle_Markup.token_markup(syntax, token) |
99 val style = Isabelle_Markup.token_markup(syntax, token) |
61 val length = token.source.length |
100 val length = token.source.length |
62 handler.handleToken(line, style, offset, length, context1) |
101 val end_offset = offset + length |
|
102 if ((offset until end_offset) exists extended.isDefinedAt) { |
|
103 for (i <- offset until end_offset) { |
|
104 val style1 = |
|
105 extended.get(i) match { |
|
106 case None => style |
|
107 case Some(ext) => ext(style) |
|
108 } |
|
109 handler.handleToken(line, style1, i, 1, context1) |
|
110 } |
|
111 } |
|
112 else handler.handleToken(line, style, offset, length, context1) |
63 offset += length |
113 offset += length |
64 } |
114 } |
65 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
115 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
66 |
116 |
67 val context2 = context1.intern |
117 val context2 = context1.intern |