1 /* |
|
2 * include isabelle's command- and keyword-declarations |
|
3 * live in jEdits syntax-highlighting |
|
4 * |
|
5 * @author Fabian Immler, TU Munich |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle.prover.Prover |
|
12 import isabelle.Markup |
|
13 |
|
14 import org.gjt.sp.jedit.buffer.JEditBuffer |
|
15 import org.gjt.sp.jedit.syntax.{Token => JToken, |
|
16 TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet} |
|
17 |
|
18 import java.awt.Color |
|
19 import java.awt.Font |
|
20 import javax.swing.text.Segment; |
|
21 |
|
22 |
|
23 object DynamicTokenMarker |
|
24 { |
|
25 /* line context */ |
|
26 |
|
27 private val rule_set = new ParserRuleSet("isabelle", "MAIN") |
|
28 private class LineContext(val line: Int, prev: LineContext) |
|
29 extends TokenMarker.LineContext(rule_set, prev) |
|
30 |
|
31 |
|
32 /* mapping to jEdit token types */ |
|
33 // TODO: as properties or CSS style sheet |
|
34 |
|
35 private val choose_byte: Map[String, Byte] = |
|
36 { |
|
37 import JToken._ |
|
38 Map[String, Byte]( |
|
39 // logical entities |
|
40 Markup.TCLASS -> LABEL, |
|
41 Markup.TYCON -> LABEL, |
|
42 Markup.FIXED_DECL -> LABEL, |
|
43 Markup.FIXED -> LABEL, |
|
44 Markup.CONST_DECL -> LABEL, |
|
45 Markup.CONST -> LABEL, |
|
46 Markup.FACT_DECL -> LABEL, |
|
47 Markup.FACT -> LABEL, |
|
48 Markup.DYNAMIC_FACT -> LABEL, |
|
49 Markup.LOCAL_FACT_DECL -> LABEL, |
|
50 Markup.LOCAL_FACT -> LABEL, |
|
51 // inner syntax |
|
52 Markup.TFREE -> LITERAL2, |
|
53 Markup.FREE -> LITERAL2, |
|
54 Markup.TVAR -> LITERAL3, |
|
55 Markup.SKOLEM -> LITERAL3, |
|
56 Markup.BOUND -> LITERAL3, |
|
57 Markup.VAR -> LITERAL3, |
|
58 Markup.NUM -> DIGIT, |
|
59 Markup.FLOAT -> DIGIT, |
|
60 Markup.XNUM -> DIGIT, |
|
61 Markup.XSTR -> LITERAL4, |
|
62 Markup.LITERAL -> LITERAL4, |
|
63 Markup.INNER_COMMENT -> COMMENT1, |
|
64 Markup.SORT -> FUNCTION, |
|
65 Markup.TYP -> FUNCTION, |
|
66 Markup.TERM -> FUNCTION, |
|
67 Markup.PROP -> FUNCTION, |
|
68 Markup.ATTRIBUTE -> FUNCTION, |
|
69 Markup.METHOD -> FUNCTION, |
|
70 // ML syntax |
|
71 Markup.ML_KEYWORD -> KEYWORD2, |
|
72 Markup.ML_IDENT -> NULL, |
|
73 Markup.ML_TVAR -> LITERAL3, |
|
74 Markup.ML_NUMERAL -> DIGIT, |
|
75 Markup.ML_CHAR -> LITERAL1, |
|
76 Markup.ML_STRING -> LITERAL1, |
|
77 Markup.ML_COMMENT -> COMMENT1, |
|
78 Markup.ML_MALFORMED -> INVALID, |
|
79 // embedded source text |
|
80 Markup.ML_SOURCE -> COMMENT4, |
|
81 Markup.DOC_SOURCE -> COMMENT4, |
|
82 Markup.ANTIQ -> COMMENT4, |
|
83 Markup.ML_ANTIQ -> COMMENT4, |
|
84 Markup.DOC_ANTIQ -> COMMENT4, |
|
85 // outer syntax |
|
86 Markup.IDENT -> NULL, |
|
87 Markup.COMMAND -> OPERATOR, |
|
88 Markup.KEYWORD -> KEYWORD4, |
|
89 Markup.VERBATIM -> COMMENT3, |
|
90 Markup.COMMENT -> COMMENT1, |
|
91 Markup.CONTROL -> COMMENT3, |
|
92 Markup.MALFORMED -> INVALID, |
|
93 Markup.STRING -> LITERAL3, |
|
94 Markup.ALTSTRING -> LITERAL1 |
|
95 ).withDefaultValue(NULL) |
|
96 } |
|
97 |
|
98 def choose_color(kind: String, styles: Array[SyntaxStyle]): Color = |
|
99 styles(choose_byte(kind)).getForegroundColor |
|
100 } |
|
101 |
|
102 |
|
103 class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) |
|
104 extends TokenMarker |
|
105 { |
|
106 override def markTokens(prev: TokenMarker.LineContext, |
|
107 handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = |
|
108 { |
|
109 val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext] |
|
110 val line = if (prev == null) 0 else previous.line + 1 |
|
111 val context = new DynamicTokenMarker.LineContext(line, previous) |
|
112 val start = buffer.getLineStartOffset(line) |
|
113 val stop = start + line_segment.count |
|
114 |
|
115 val theory_view = Isabelle.prover_setup(buffer).get.theory_view |
|
116 val document = theory_view.current_document() |
|
117 def to: Int => Int = theory_view.to_current(document, _) |
|
118 def from: Int => Int = theory_view.from_current(document, _) |
|
119 |
|
120 var next_x = start |
|
121 var cmd = document.command_at(from(start)) |
|
122 while (cmd.isDefined && cmd.get.start(document) < from(stop)) { |
|
123 val command = cmd.get |
|
124 for { |
|
125 markup <- command.highlight(document).flatten |
|
126 command_start = command.start(document) |
|
127 abs_start = to(command_start + markup.start) |
|
128 abs_stop = to(command_start + markup.stop) |
|
129 if (abs_stop > start) |
|
130 if (abs_start < stop) |
|
131 byte = DynamicTokenMarker.choose_byte(markup.info.toString) |
|
132 token_start = (abs_start - start) max 0 |
|
133 token_length = |
|
134 (abs_stop - abs_start) - |
|
135 ((start - abs_start) max 0) - |
|
136 ((abs_stop - stop) max 0) |
|
137 } { |
|
138 if (start + token_start > next_x) |
|
139 handler.handleToken(line_segment, 1, |
|
140 next_x - start, start + token_start - next_x, context) |
|
141 handler.handleToken(line_segment, byte, |
|
142 token_start, token_length, context) |
|
143 next_x = start + token_start + token_length |
|
144 } |
|
145 cmd = document.commands.next(command) |
|
146 } |
|
147 if (next_x < stop) |
|
148 handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context) |
|
149 |
|
150 handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context) |
|
151 handler.setLineContext(context) |
|
152 return context |
|
153 } |
|
154 } |
|