author | wenzelm |
Sat, 28 Aug 2010 20:24:41 +0200 | |
changeset 38843 | d95522496593 |
parent 38641 | 7ab0ae836f74 |
child 38845 | a9e37daf5bd0 |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/document_model.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
5 |
Document model connected to jEdit buffer -- single node in theory graph. |
36760 | 6 |
*/ |
34407 | 7 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
8 |
package isabelle.jedit |
34760 | 9 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
36015 | 11 |
import isabelle._ |
12 |
||
34693 | 13 |
import scala.collection.mutable |
34446 | 14 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
15 |
import org.gjt.sp.jedit.Buffer |
34783
cb95d6bbf5f1
clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents:
34778
diff
changeset
|
16 |
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} |
38158 | 17 |
import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet} |
18 |
import org.gjt.sp.jedit.textarea.TextArea |
|
19 |
||
20 |
import java.awt.font.TextAttribute |
|
21 |
import javax.swing.text.Segment; |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
|
34760 | 23 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
24 |
object Document_Model |
34588 | 25 |
{ |
38158 | 26 |
object Token_Markup |
27 |
{ |
|
28 |
/* extended token styles */ |
|
29 |
||
30 |
private val plain_range: Int = Token.ID_COUNT |
|
31 |
private val full_range: Int = 3 * plain_range |
|
32 |
private def check_range(i: Int) { require(0 <= i && i < plain_range) } |
|
33 |
||
34 |
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } |
|
35 |
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } |
|
36 |
||
37 |
private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = |
|
38 |
{ |
|
39 |
import scala.collection.JavaConversions._ |
|
40 |
val script_font = |
|
41 |
style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))) |
|
42 |
new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font) |
|
43 |
} |
|
44 |
||
45 |
def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = |
|
46 |
{ |
|
47 |
val new_styles = new Array[SyntaxStyle](full_range) |
|
48 |
for (i <- 0 until plain_range) { |
|
49 |
val style = styles(i) |
|
50 |
new_styles(i) = style |
|
51 |
new_styles(subscript(i.toByte)) = script_style(style, -1) |
|
52 |
new_styles(superscript(i.toByte)) = script_style(style, 1) |
|
53 |
} |
|
54 |
new_styles |
|
55 |
} |
|
56 |
||
57 |
||
58 |
/* line context */ |
|
59 |
||
60 |
private val rule_set = new ParserRuleSet("isabelle", "MAIN") |
|
61 |
class LineContext(val line: Int, prev: LineContext) |
|
62 |
extends TokenMarker.LineContext(rule_set, prev) |
|
63 |
||
64 |
||
65 |
/* mapping to jEdit token types */ |
|
66 |
// TODO: as properties or CSS style sheet |
|
67 |
||
68 |
val command_style: Map[String, Byte] = |
|
69 |
{ |
|
70 |
import Token._ |
|
71 |
Map[String, Byte]( |
|
72 |
Keyword.THY_END -> KEYWORD2, |
|
73 |
Keyword.THY_SCRIPT -> LABEL, |
|
74 |
Keyword.PRF_SCRIPT -> LABEL, |
|
75 |
Keyword.PRF_ASM -> KEYWORD3, |
|
76 |
Keyword.PRF_ASM_GOAL -> KEYWORD3 |
|
77 |
).withDefaultValue(KEYWORD1) |
|
78 |
} |
|
79 |
||
80 |
val token_style: Map[String, Byte] = |
|
81 |
{ |
|
82 |
import Token._ |
|
83 |
Map[String, Byte]( |
|
84 |
// logical entities |
|
85 |
Markup.TCLASS -> NULL, |
|
86 |
Markup.TYCON -> NULL, |
|
87 |
Markup.FIXED_DECL -> FUNCTION, |
|
88 |
Markup.FIXED -> NULL, |
|
89 |
Markup.CONST_DECL -> FUNCTION, |
|
90 |
Markup.CONST -> NULL, |
|
91 |
Markup.FACT_DECL -> FUNCTION, |
|
92 |
Markup.FACT -> NULL, |
|
93 |
Markup.DYNAMIC_FACT -> LABEL, |
|
94 |
Markup.LOCAL_FACT_DECL -> FUNCTION, |
|
95 |
Markup.LOCAL_FACT -> NULL, |
|
96 |
// inner syntax |
|
97 |
Markup.TFREE -> NULL, |
|
98 |
Markup.FREE -> NULL, |
|
99 |
Markup.TVAR -> NULL, |
|
100 |
Markup.SKOLEM -> NULL, |
|
101 |
Markup.BOUND -> NULL, |
|
102 |
Markup.VAR -> NULL, |
|
103 |
Markup.NUM -> DIGIT, |
|
104 |
Markup.FLOAT -> DIGIT, |
|
105 |
Markup.XNUM -> DIGIT, |
|
106 |
Markup.XSTR -> LITERAL4, |
|
107 |
Markup.LITERAL -> OPERATOR, |
|
108 |
Markup.INNER_COMMENT -> COMMENT1, |
|
109 |
Markup.SORT -> NULL, |
|
110 |
Markup.TYP -> NULL, |
|
111 |
Markup.TERM -> NULL, |
|
112 |
Markup.PROP -> NULL, |
|
113 |
Markup.ATTRIBUTE -> NULL, |
|
114 |
Markup.METHOD -> NULL, |
|
115 |
// ML syntax |
|
116 |
Markup.ML_KEYWORD -> KEYWORD1, |
|
117 |
Markup.ML_DELIMITER -> OPERATOR, |
|
118 |
Markup.ML_IDENT -> NULL, |
|
119 |
Markup.ML_TVAR -> NULL, |
|
120 |
Markup.ML_NUMERAL -> DIGIT, |
|
121 |
Markup.ML_CHAR -> LITERAL1, |
|
122 |
Markup.ML_STRING -> LITERAL1, |
|
123 |
Markup.ML_COMMENT -> COMMENT1, |
|
124 |
Markup.ML_MALFORMED -> INVALID, |
|
125 |
// embedded source text |
|
126 |
Markup.ML_SOURCE -> COMMENT3, |
|
127 |
Markup.DOC_SOURCE -> COMMENT3, |
|
128 |
Markup.ANTIQ -> COMMENT4, |
|
129 |
Markup.ML_ANTIQ -> COMMENT4, |
|
130 |
Markup.DOC_ANTIQ -> COMMENT4, |
|
131 |
// outer syntax |
|
132 |
Markup.KEYWORD -> KEYWORD2, |
|
133 |
Markup.OPERATOR -> OPERATOR, |
|
134 |
Markup.COMMAND -> KEYWORD1, |
|
135 |
Markup.IDENT -> NULL, |
|
136 |
Markup.VERBATIM -> COMMENT3, |
|
137 |
Markup.COMMENT -> COMMENT1, |
|
138 |
Markup.CONTROL -> COMMENT3, |
|
139 |
Markup.MALFORMED -> INVALID, |
|
140 |
Markup.STRING -> LITERAL3, |
|
141 |
Markup.ALTSTRING -> LITERAL1 |
|
142 |
).withDefaultValue(NULL) |
|
143 |
} |
|
144 |
} |
|
145 |
||
146 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
147 |
/* document model of buffer */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
148 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
149 |
private val key = "isabelle.document_model" |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
150 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
151 |
def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = |
34716 | 152 |
{ |
38223 | 153 |
Swing_Thread.require() |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
154 |
val model = new Document_Model(session, buffer, thy_name) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
155 |
buffer.setProperty(key, model) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
156 |
model.activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
157 |
model |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
158 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
159 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
160 |
def apply(buffer: Buffer): Option[Document_Model] = |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
161 |
{ |
38223 | 162 |
Swing_Thread.require() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
163 |
buffer.getProperty(key) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
164 |
case model: Document_Model => Some(model) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
165 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
166 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
167 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
168 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
169 |
def exit(buffer: Buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
170 |
{ |
38223 | 171 |
Swing_Thread.require() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
172 |
apply(buffer) match { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
173 |
case None => error("No document model for buffer: " + buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
174 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
175 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
176 |
buffer.unsetProperty(key) |
34653 | 177 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
178 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
179 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
180 |
|
38151 | 181 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
182 |
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) |
34588 | 183 |
{ |
37555
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
184 |
/* visible line end */ |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
185 |
|
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
186 |
// simplify slightly odd result of TextArea.getLineEndOffset |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
187 |
// NB: jEdit already normalizes \r\n and \r to \n |
38426 | 188 |
def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset = |
37555
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
189 |
{ |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
190 |
val end1 = end - 1 |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
191 |
if (start <= end1 && end1 < buffer.getLength && |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
192 |
buffer.getSegment(end1, 1).charAt(0) == '\n') end1 |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
193 |
else end |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
194 |
} |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
195 |
|
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
196 |
|
38224 | 197 |
/* pending text edits */ |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
198 |
|
38224 | 199 |
object pending_edits // owned by Swing thread |
200 |
{ |
|
38425 | 201 |
private val pending = new mutable.ListBuffer[Text.Edit] |
202 |
def snapshot(): List[Text.Edit] = pending.toList |
|
38224 | 203 |
|
204 |
private val delay_flush = Swing_Thread.delay_last(session.input_delay) { |
|
38417 | 205 |
if (!pending.isEmpty) session.edit_version(List((thy_name, flush()))) |
38224 | 206 |
} |
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
207 |
|
38425 | 208 |
def flush(): List[Text.Edit] = |
38224 | 209 |
{ |
210 |
Swing_Thread.require() |
|
211 |
val edits = snapshot() |
|
212 |
pending.clear |
|
213 |
edits |
|
214 |
} |
|
215 |
||
38425 | 216 |
def +=(edit: Text.Edit) |
38224 | 217 |
{ |
218 |
Swing_Thread.require() |
|
219 |
pending += edit |
|
220 |
delay_flush() |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
221 |
} |
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
222 |
} |
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
223 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
224 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
225 |
/* snapshot */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
226 |
|
38417 | 227 |
def snapshot(): Document.Snapshot = |
228 |
{ |
|
38223 | 229 |
Swing_Thread.require() |
38359
96b22dfeb56a
consider snapshot as service of Session, not Document.Change;
wenzelm
parents:
38356
diff
changeset
|
230 |
session.snapshot(thy_name, pending_edits.snapshot()) |
38223 | 231 |
} |
34828 | 232 |
|
233 |
||
234 |
/* buffer listener */ |
|
235 |
||
236 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
237 |
{ |
|
238 |
override def contentInserted(buffer: JEditBuffer, |
|
239 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
240 |
{ |
|
38425 | 241 |
pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) |
34828 | 242 |
} |
243 |
||
244 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 245 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 246 |
{ |
38426 | 247 |
pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) |
34828 | 248 |
} |
249 |
} |
|
250 |
||
251 |
||
38158 | 252 |
/* semantic token marker */ |
253 |
||
254 |
private val token_marker = new TokenMarker |
|
255 |
{ |
|
256 |
override def markTokens(prev: TokenMarker.LineContext, |
|
257 |
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = |
|
258 |
{ |
|
38843 | 259 |
Isabelle.swing_buffer_lock(buffer) { |
260 |
val snapshot = Document_Model.this.snapshot() |
|
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
261 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
262 |
val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext] |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
263 |
val line = if (prev == null) 0 else previous.line + 1 |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
264 |
val context = new Document_Model.Token_Markup.LineContext(line, previous) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
265 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
266 |
val start = buffer.getLineStartOffset(line) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
267 |
val stop = start + line_segment.count |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
268 |
val range = Text.Range(start, stop) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
269 |
val former_range = snapshot.revert(range) |
38158 | 270 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
271 |
/* FIXME |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
272 |
for (text_area <- Isabelle.jedit_text_areas(buffer) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
273 |
if Document_View(text_area).isDefined) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
274 |
Document_View(text_area).get.set_styles() |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
275 |
*/ |
38158 | 276 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
277 |
def handle_token(style: Byte, offset: Text.Offset, length: Int) = |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
278 |
handler.handleToken(line_segment, style, offset, length, context) |
34680 | 279 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
280 |
val syntax = session.current_syntax() |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
281 |
val token_markup: PartialFunction[Text.Info[Any], Byte] = |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
282 |
{ |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
283 |
case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
284 |
if syntax.keyword_kind(name).isDefined => |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
285 |
Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
286 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
287 |
case Text.Info(_, XML.Elem(Markup(name, _), _)) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
288 |
if Document_Model.Token_Markup.token_style(name) != Token.NULL => |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
289 |
Document_Model.Token_Markup.token_style(name) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
290 |
} |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
291 |
|
38641
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
292 |
var next_x = start |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
293 |
for { |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
294 |
(command, command_start) <- snapshot.node.command_range(former_range) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
295 |
info <- snapshot.state(command).markup. |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
296 |
select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
297 |
val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
298 |
if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
299 |
} |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
300 |
{ |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
301 |
val token_start = (abs_start - start) max 0 |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
302 |
val token_length = |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
303 |
(abs_stop - abs_start) - |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
304 |
((start - abs_start) max 0) - |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
305 |
((abs_stop - stop) max 0) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
306 |
if (start + token_start > next_x) // FIXME ?? |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
307 |
handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
308 |
handle_token(info.info, token_start, token_length) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
309 |
next_x = start + token_start + token_length |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
310 |
} |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
311 |
if (next_x < stop) // FIXME ?? |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
312 |
handle_token(Token.COMMENT1, next_x - start, stop - next_x) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
313 |
|
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
314 |
handle_token(Token.END, line_segment.count, 0) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
315 |
handler.setLineContext(context) |
7ab0ae836f74
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm
parents:
38637
diff
changeset
|
316 |
context |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
317 |
} |
38158 | 318 |
} |
319 |
} |
|
320 |
||
321 |
||
322 |
/* activation */ |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
323 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
324 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
325 |
{ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
326 |
buffer.setTokenMarker(token_marker) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
327 |
buffer.addBufferListener(buffer_listener) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
328 |
buffer.propertiesChanged() |
38425 | 329 |
pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength)) |
34680 | 330 |
} |
331 |
||
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
332 |
def refresh() |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
333 |
{ |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
334 |
buffer.setTokenMarker(token_marker) |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
335 |
} |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
336 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
337 |
def deactivate() |
34680 | 338 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
339 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
340 |
buffer.removeBufferListener(buffer_listener) |
34680 | 341 |
} |
34447 | 342 |
} |