author | wenzelm |
Tue, 14 Jun 2011 17:24:23 +0200 | |
changeset 43390 | 7ee98a3802af |
parent 43282 | 5d294220ca43 |
child 43394 | 47e60a27a496 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
40851
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/document_model.scala |
36760 | 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 |
/* line context */ |
|
29 |
||
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
|
30 |
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
|
31 |
|
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
|
32 |
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
|
33 |
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
|
34 |
{ |
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
|
35 |
override def hashCode: Int = line |
40851 | 36 |
override def equals(that: Any): Boolean = |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
} |
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
|
41 |
} |
38158 | 42 |
} |
43 |
||
44 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
45 |
/* 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
|
46 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
47 |
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
|
48 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
49 |
def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = |
34716 | 50 |
{ |
38223 | 51 |
Swing_Thread.require() |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
model.activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
55 |
model |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
56 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
57 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
58 |
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
|
59 |
{ |
38223 | 60 |
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
|
61 |
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
|
62 |
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
|
63 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
64 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
65 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
66 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
67 |
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
|
68 |
{ |
38223 | 69 |
Swing_Thread.require() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
70 |
apply(buffer) match { |
39636 | 71 |
case None => |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
72 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
73 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
74 |
buffer.unsetProperty(key) |
34653 | 75 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
76 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
77 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
78 |
|
38151 | 79 |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
80 |
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) |
34588 | 81 |
{ |
38224 | 82 |
/* pending text edits */ |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
83 |
|
38224 | 84 |
object pending_edits // owned by Swing thread |
85 |
{ |
|
38425 | 86 |
private val pending = new mutable.ListBuffer[Text.Edit] |
87 |
def snapshot(): List[Text.Edit] = pending.toList |
|
38224 | 88 |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
89 |
def flush(more_edits: Option[List[Text.Edit]]*) |
38224 | 90 |
{ |
91 |
Swing_Thread.require() |
|
92 |
val edits = snapshot() |
|
93 |
pending.clear |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
94 |
|
40481 | 95 |
val all_edits = |
96 |
if (edits.isEmpty) more_edits.toList |
|
97 |
else Some(edits) :: more_edits.toList |
|
98 |
if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _))) |
|
38224 | 99 |
} |
100 |
||
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
101 |
def init() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
102 |
{ |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
103 |
Swing_Thread.require() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
104 |
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
|
105 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
106 |
|
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
107 |
private val delay_flush = |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
108 |
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
|
109 |
|
38425 | 110 |
def +=(edit: Text.Edit) |
38224 | 111 |
{ |
112 |
Swing_Thread.require() |
|
113 |
pending += edit |
|
114 |
delay_flush() |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
115 |
} |
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
116 |
} |
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
117 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
118 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
119 |
/* snapshot */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
120 |
|
38417 | 121 |
def snapshot(): Document.Snapshot = |
122 |
{ |
|
38223 | 123 |
Swing_Thread.require() |
38359
96b22dfeb56a
consider snapshot as service of Session, not Document.Change;
wenzelm
parents:
38356
diff
changeset
|
124 |
session.snapshot(thy_name, pending_edits.snapshot()) |
38223 | 125 |
} |
34828 | 126 |
|
127 |
||
128 |
/* buffer listener */ |
|
129 |
||
130 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
131 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
132 |
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
|
133 |
{ |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
134 |
pending_edits.init() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
135 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
136 |
|
34828 | 137 |
override def contentInserted(buffer: JEditBuffer, |
138 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
139 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
140 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
141 |
pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) |
34828 | 142 |
} |
143 |
||
144 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 145 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 146 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
147 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
148 |
pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) |
34828 | 149 |
} |
150 |
} |
|
151 |
||
152 |
||
38158 | 153 |
/* semantic token marker */ |
154 |
||
155 |
private val token_marker = new TokenMarker |
|
156 |
{ |
|
157 |
override def markTokens(prev: TokenMarker.LineContext, |
|
158 |
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = |
|
159 |
{ |
|
38843 | 160 |
Isabelle.swing_buffer_lock(buffer) { |
161 |
val snapshot = Document_Model.this.snapshot() |
|
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
162 |
|
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
|
163 |
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
|
164 |
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
|
165 |
val context = new Document_Model.Token_Markup.Line_Context(line, previous) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
166 |
|
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
|
167 |
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
|
168 |
val stop = start + line_segment.count |
38158 | 169 |
|
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
|
170 |
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
|
171 |
handler.handleToken(line_segment, style, offset, length, context) |
34680 | 172 |
|
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
|
173 |
val syntax = session.current_syntax() |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
174 |
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
|
175 |
|
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
176 |
var last = start |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
177 |
for (token <- tokens.iterator) { |
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
178 |
val Text.Range(token_start, token_stop) = token.range |
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
179 |
if (last < token_start) |
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
180 |
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
|
181 |
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
|
182 |
token_start - start, token_stop - token_start) |
38846
e54c33dbe77c
Document_Model.token_marker: misc tuning and simplification;
wenzelm
parents:
38845
diff
changeset
|
183 |
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
|
184 |
} |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
185 |
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
|
186 |
|
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
|
187 |
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
|
188 |
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
|
189 |
context |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38569
diff
changeset
|
190 |
} |
38158 | 191 |
} |
192 |
} |
|
193 |
||
194 |
||
195 |
/* activation */ |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
196 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
197 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
198 |
{ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
199 |
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
|
200 |
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
|
201 |
buffer.propertiesChanged() |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
202 |
pending_edits.init() |
34680 | 203 |
} |
204 |
||
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
205 |
def refresh() |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
206 |
{ |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
207 |
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
|
208 |
} |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
209 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
210 |
def deactivate() |
34680 | 211 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
212 |
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
|
213 |
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
|
214 |
buffer.removeBufferListener(buffer_listener) |
34680 | 215 |
} |
34447 | 216 |
} |