author | wenzelm |
Thu, 11 Nov 2010 16:48:46 +0100 | |
changeset 40478 | 4bae781b8f7c |
parent 40474 | 576b88b1dce9 |
child 40481 | da2c56aaaa68 |
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 |
||
38852
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
60 |
private val dummy_rules = new ParserRuleSet("isabelle", "MAIN") |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
61 |
|
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
62 |
class Line_Context(val line: Int, prev: Line_Context) |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
63 |
extends TokenMarker.LineContext(dummy_rules, prev) |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
64 |
{ |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
65 |
override def hashCode: Int = line |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
66 |
override def equals(that: Any) = |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
67 |
that match { |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
68 |
case other: Line_Context => line == other.line |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
69 |
case _ => false |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
70 |
} |
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
71 |
} |
38158 | 72 |
} |
73 |
||
74 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
75 |
/* 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
|
76 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
77 |
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
|
78 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
79 |
def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = |
34716 | 80 |
{ |
38223 | 81 |
Swing_Thread.require() |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
model.activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
85 |
model |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
86 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
87 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
88 |
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
|
89 |
{ |
38223 | 90 |
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
|
91 |
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
|
92 |
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
|
93 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
94 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
95 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
96 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
97 |
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
|
98 |
{ |
38223 | 99 |
Swing_Thread.require() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
100 |
apply(buffer) match { |
39636 | 101 |
case None => |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
102 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
103 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
104 |
buffer.unsetProperty(key) |
34653 | 105 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
106 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
107 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
108 |
|
38151 | 109 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
110 |
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) |
34588 | 111 |
{ |
38224 | 112 |
/* pending text edits */ |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
113 |
|
38224 | 114 |
object pending_edits // owned by Swing thread |
115 |
{ |
|
38425 | 116 |
private val pending = new mutable.ListBuffer[Text.Edit] |
117 |
def snapshot(): List[Text.Edit] = pending.toList |
|
38224 | 118 |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
119 |
def flush(more_edits: Option[List[Text.Edit]]*) |
38224 | 120 |
{ |
121 |
Swing_Thread.require() |
|
122 |
val edits = snapshot() |
|
123 |
pending.clear |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
124 |
|
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
125 |
if (!edits.isEmpty || !more_edits.isEmpty) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
126 |
session.edit_version((Some(edits) :: more_edits.toList).map((thy_name, _))) |
38224 | 127 |
} |
128 |
||
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
129 |
def init() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
130 |
{ |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
131 |
Swing_Thread.require() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
132 |
flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer))))) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
133 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
134 |
|
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
135 |
private val delay_flush = |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
136 |
Swing_Thread.delay_last(session.input_delay) { flush() } |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
137 |
|
38425 | 138 |
def +=(edit: Text.Edit) |
38224 | 139 |
{ |
140 |
Swing_Thread.require() |
|
141 |
pending += edit |
|
142 |
delay_flush() |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
143 |
} |
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
144 |
} |
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
145 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
146 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
147 |
/* snapshot */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
148 |
|
38417 | 149 |
def snapshot(): Document.Snapshot = |
150 |
{ |
|
38223 | 151 |
Swing_Thread.require() |
38359
96b22dfeb56a
consider snapshot as service of Session, not Document.Change;
wenzelm
parents:
38356
diff
changeset
|
152 |
session.snapshot(thy_name, pending_edits.snapshot()) |
38223 | 153 |
} |
34828 | 154 |
|
155 |
||
156 |
/* buffer listener */ |
|
157 |
||
158 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
159 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
160 |
override def bufferLoaded(buffer: JEditBuffer) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
161 |
{ |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
162 |
pending_edits.init() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
163 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
164 |
|
34828 | 165 |
override def contentInserted(buffer: JEditBuffer, |
166 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
167 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
168 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
169 |
pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) |
34828 | 170 |
} |
171 |
||
172 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 173 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 174 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
175 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
176 |
pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) |
34828 | 177 |
} |
178 |
} |
|
179 |
||
180 |
||
38158 | 181 |
/* semantic token marker */ |
182 |
||
183 |
private val token_marker = new TokenMarker |
|
184 |
{ |
|
185 |
override def markTokens(prev: TokenMarker.LineContext, |
|
186 |
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = |
|
187 |
{ |
|
38843 | 188 |
Isabelle.swing_buffer_lock(buffer) { |
189 |
val snapshot = Document_Model.this.snapshot() |
|
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
190 |
|
38852
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
191 |
val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context] |
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
|
192 |
val line = if (prev == null) 0 else previous.line + 1 |
38852
23513fb32e7b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;
wenzelm
parents:
38846
diff
changeset
|
193 |
val context = new Document_Model.Token_Markup.Line_Context(line, previous) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
194 |
|
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
|
195 |
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
|
196 |
val stop = start + line_segment.count |
38158 | 197 |
|
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
|
198 |
/* 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
|
199 |
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
|
200 |
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
|
201 |
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
|
202 |
*/ |
38158 | 203 |
|
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
|
204 |
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
|
205 |
handler.handleToken(line_segment, style, offset, length, context) |
34680 | 206 |
|
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
|
207 |
val syntax = session.current_syntax() |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
208 |
val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax)) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
209 |
|
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
210 |
var last = start |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
211 |
for (token <- tokens.iterator) { |
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
212 |
val Text.Range(token_start, token_stop) = token.range |
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
213 |
if (last < token_start) |
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
214 |
handle_token(Token.COMMENT1, last - start, token_start - last) |
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38880
diff
changeset
|
215 |
handle_token(token.info getOrElse Token.NULL, |
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38880
diff
changeset
|
216 |
token_start - start, token_stop - token_start) |
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
217 |
last = token_stop |
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
|
218 |
} |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
219 |
if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last) |
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
|
220 |
|
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
|
221 |
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
|
222 |
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
|
223 |
context |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
224 |
} |
38158 | 225 |
} |
226 |
} |
|
227 |
||
228 |
||
229 |
/* activation */ |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
230 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
231 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
232 |
{ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
233 |
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
|
234 |
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
|
235 |
buffer.propertiesChanged() |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
236 |
pending_edits.init() |
34680 | 237 |
} |
238 |
||
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
239 |
def refresh() |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
240 |
{ |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
241 |
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
|
242 |
} |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
243 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
244 |
def deactivate() |
34680 | 245 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
246 |
pending_edits.flush() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
247 |
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
|
248 |
buffer.removeBufferListener(buffer_listener) |
34680 | 249 |
} |
34447 | 250 |
} |