author | wenzelm |
Mon, 12 Aug 2013 12:06:48 +0200 | |
changeset 52974 | 908e8a36e975 |
parent 52973 | d5f7fa1498b7 |
child 52977 | 15254e32d299 |
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.textarea.TextArea |
18 |
||
19 |
import java.awt.font.TextAttribute |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
|
34760 | 21 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
22 |
object Document_Model |
34588 | 23 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
24 |
/* 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
|
25 |
|
50565 | 26 |
private val key = "PIDE.document_model" |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
27 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
28 |
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
|
29 |
{ |
38223 | 30 |
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
|
31 |
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
|
32 |
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
|
33 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
34 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
35 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
36 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
37 |
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
|
38 |
{ |
38223 | 39 |
Swing_Thread.require() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
40 |
apply(buffer) match { |
39636 | 41 |
case None => |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
42 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
43 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
44 |
buffer.unsetProperty(key) |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
45 |
buffer.propertiesChanged |
34653 | 46 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
47 |
} |
43397 | 48 |
|
52973 | 49 |
def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = |
43397 | 50 |
{ |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
51 |
Swing_Thread.require() |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
52 |
apply(buffer).map(_.deactivate) |
52973 | 53 |
val model = new Document_Model(session, buffer, node_name) |
43397 | 54 |
buffer.setProperty(key, model) |
55 |
model.activate() |
|
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
56 |
buffer.propertiesChanged |
43397 | 57 |
model |
58 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
59 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
60 |
|
38151 | 61 |
|
52973 | 62 |
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
34588 | 63 |
{ |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
64 |
/* header */ |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
65 |
|
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
66 |
def node_header(): Document.Node.Header = |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
67 |
{ |
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
68 |
Swing_Thread.require() |
49406 | 69 |
JEdit_Lib.buffer_lock(buffer) { |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
70 |
Exn.capture { |
52973 | 71 |
PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
72 |
} match { |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
73 |
case Exn.Res(header) => header |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
74 |
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
75 |
} |
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
76 |
} |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
77 |
} |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
78 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
79 |
|
52849 | 80 |
/* overlays */ |
81 |
||
52887 | 82 |
private var overlays = Document.Node.Overlays.empty |
52849 | 83 |
|
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52859
diff
changeset
|
84 |
def insert_overlay(command: Command, name: String, args: List[String]): Unit = |
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52859
diff
changeset
|
85 |
Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } |
52849 | 86 |
|
52858
863581a704a6
avoid repeated PIDE.flush_buffers when manipulating overlays;
wenzelm
parents:
52849
diff
changeset
|
87 |
def remove_overlay(command: Command, name: String, args: List[String]): Unit = |
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52859
diff
changeset
|
88 |
Swing_Thread.require { overlays = overlays.remove(command, (name, args)) } |
52849 | 89 |
|
90 |
||
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
91 |
/* perspective */ |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
92 |
|
52849 | 93 |
// owned by Swing thread |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
94 |
private var _node_required = false |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
95 |
def node_required: Boolean = _node_required |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
96 |
def node_required_=(b: Boolean) |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
97 |
{ |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
98 |
Swing_Thread.require() |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
99 |
if (_node_required != b) { |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
100 |
_node_required = b |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
101 |
PIDE.options_changed() |
52974 | 102 |
PIDE.editor.flush() |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
103 |
} |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
104 |
} |
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52807
diff
changeset
|
105 |
|
52849 | 106 |
val empty_perspective: Document.Node.Perspective_Text = |
52887 | 107 |
Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty) |
52849 | 108 |
|
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52807
diff
changeset
|
109 |
def node_perspective(): Document.Node.Perspective_Text = |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
110 |
{ |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
111 |
Swing_Thread.require() |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
112 |
|
52849 | 113 |
if (Isabelle.continuous_checking) { |
114 |
Document.Node.Perspective(node_required, Text.Perspective( |
|
115 |
for { |
|
116 |
doc_view <- PIDE.document_views(buffer) |
|
117 |
range <- doc_view.perspective().ranges |
|
118 |
} yield range), overlays) |
|
119 |
} |
|
120 |
else empty_perspective |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
121 |
} |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
122 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
123 |
|
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
124 |
/* edits */ |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
125 |
|
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
126 |
def init_edits(): List[Document.Edit_Text] = |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
127 |
{ |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
128 |
Swing_Thread.require() |
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
52808
diff
changeset
|
129 |
|
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
130 |
val header = node_header() |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
131 |
val text = JEdit_Lib.buffer_text(buffer) |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
132 |
val perspective = node_perspective() |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
133 |
|
52973 | 134 |
List(session.header_edit(node_name, header), |
135 |
node_name -> Document.Node.Clear(), |
|
136 |
node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), |
|
137 |
node_name -> perspective) |
|
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
138 |
} |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
139 |
|
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52807
diff
changeset
|
140 |
def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) |
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
141 |
: List[Document.Edit_Text] = |
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
142 |
{ |
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
143 |
Swing_Thread.require() |
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
52808
diff
changeset
|
144 |
|
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
145 |
val header = node_header() |
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
146 |
|
52973 | 147 |
List(session.header_edit(node_name, header), |
148 |
node_name -> Document.Node.Edits(text_edits), |
|
149 |
node_name -> perspective) |
|
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
150 |
} |
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
151 |
|
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
152 |
|
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
153 |
/* pending edits */ |
43648 | 154 |
|
43644 | 155 |
private object pending_edits // owned by Swing thread |
38224 | 156 |
{ |
38425 | 157 |
private val pending = new mutable.ListBuffer[Text.Edit] |
52849 | 158 |
private var last_perspective = empty_perspective |
44438 | 159 |
|
38425 | 160 |
def snapshot(): List[Text.Edit] = pending.toList |
38224 | 161 |
|
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
162 |
def flushed_edits(): List[Document.Edit_Text] = |
38224 | 163 |
{ |
164 |
Swing_Thread.require() |
|
44438 | 165 |
|
47393
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
166 |
val edits = snapshot() |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
167 |
val new_perspective = node_perspective() |
47393
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
168 |
if (!edits.isEmpty || last_perspective != new_perspective) { |
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
169 |
pending.clear |
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
170 |
last_perspective = new_perspective |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
171 |
node_edits(new_perspective, edits) |
43648 | 172 |
} |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
173 |
else Nil |
38224 | 174 |
} |
175 |
||
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
176 |
def flush(): Unit = session.update(flushed_edits()) |
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
177 |
|
52767
9c28559e5fff
back to model.update_perspective with delay (cf. a20631db9c8a);
wenzelm
parents:
52759
diff
changeset
|
178 |
val delay_flush = |
50207 | 179 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
180 |
|
38425 | 181 |
def +=(edit: Text.Edit) |
38224 | 182 |
{ |
183 |
Swing_Thread.require() |
|
184 |
pending += edit |
|
49195 | 185 |
delay_flush.invoke() |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
186 |
} |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
187 |
|
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
188 |
def init() |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
189 |
{ |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
190 |
flush() |
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
191 |
session.update(init_edits()) |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
192 |
} |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
193 |
|
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
194 |
def exit() |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
195 |
{ |
49195 | 196 |
delay_flush.revoke() |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
197 |
flush() |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
198 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
199 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
200 |
|
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
201 |
def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits() |
52767
9c28559e5fff
back to model.update_perspective with delay (cf. a20631db9c8a);
wenzelm
parents:
52759
diff
changeset
|
202 |
|
9c28559e5fff
back to model.update_perspective with delay (cf. a20631db9c8a);
wenzelm
parents:
52759
diff
changeset
|
203 |
def update_perspective(): Unit = pending_edits.delay_flush.invoke() |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44615
diff
changeset
|
204 |
|
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
205 |
|
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
206 |
/* snapshot */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
207 |
|
38417 | 208 |
def snapshot(): Document.Snapshot = |
209 |
{ |
|
38223 | 210 |
Swing_Thread.require() |
52973 | 211 |
session.snapshot(node_name, pending_edits.snapshot()) |
38223 | 212 |
} |
34828 | 213 |
|
214 |
||
215 |
/* buffer listener */ |
|
216 |
||
217 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
218 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
219 |
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
|
220 |
{ |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
221 |
pending_edits.init() |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
222 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
223 |
|
34828 | 224 |
override def contentInserted(buffer: JEditBuffer, |
225 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
226 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
227 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
228 |
pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) |
34828 | 229 |
} |
230 |
||
231 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 232 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 233 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
234 |
if (!buffer.isLoading) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
235 |
pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) |
34828 | 236 |
} |
237 |
} |
|
238 |
||
239 |
||
38158 | 240 |
/* activation */ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
241 |
|
43512 | 242 |
private def activate() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
243 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
244 |
buffer.addBufferListener(buffer_listener) |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
245 |
pending_edits.flush() |
44358
2a2df4de1bbe
more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents:
44182
diff
changeset
|
246 |
Token_Markup.refresh_buffer(buffer) |
34680 | 247 |
} |
248 |
||
43512 | 249 |
private def deactivate() |
34680 | 250 |
{ |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46739
diff
changeset
|
251 |
pending_edits.exit() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
252 |
buffer.removeBufferListener(buffer_listener) |
44358
2a2df4de1bbe
more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents:
44182
diff
changeset
|
253 |
Token_Markup.refresh_buffer(buffer) |
34680 | 254 |
} |
34447 | 255 |
} |