author | wenzelm |
Sun, 08 Jan 2017 12:31:45 +0100 | |
changeset 64831 | 4792ee012e94 |
parent 64829 | 07f209e957bc |
child 64832 | f6a09ac4e640 |
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 |
||
64817 | 5 |
Document model connected to jEdit buffer or external file: content of theory |
6 |
node or auxiliary file (blob). |
|
36760 | 7 |
*/ |
34407 | 8 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
9 |
package isabelle.jedit |
34760 | 10 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
36015 | 12 |
import isabelle._ |
13 |
||
34693 | 14 |
import scala.collection.mutable |
34446 | 15 |
|
64817 | 16 |
import org.gjt.sp.jedit.{jEdit, View} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
17 |
import org.gjt.sp.jedit.Buffer |
61192 | 18 |
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
|
34760 | 20 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
21 |
object Document_Model |
34588 | 22 |
{ |
64817 | 23 |
/* document models */ |
24 |
||
25 |
sealed case class State( |
|
26 |
models: Map[Document.Node.Name, Document_Model] = Map.empty, |
|
27 |
buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty) |
|
28 |
{ |
|
29 |
def models_iterator: Iterator[Document_Model] = |
|
30 |
for ((_, model) <- models.iterator) yield model |
|
64813 | 31 |
|
64817 | 32 |
def file_models_iterator: Iterator[File_Model] = |
33 |
for { |
|
34 |
(_, model) <- models.iterator |
|
35 |
if model.isInstanceOf[File_Model] |
|
36 |
} yield model.asInstanceOf[File_Model] |
|
64813 | 37 |
|
64817 | 38 |
def buffer_models_iterator: Iterator[Buffer_Model] = |
39 |
for ((_, model) <- buffer_models.iterator) yield model |
|
64813 | 40 |
|
41 |
||
64817 | 42 |
def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) |
43 |
: (Buffer_Model, State) = |
|
44 |
{ |
|
45 |
val old_model = |
|
46 |
models.get(node_name) match { |
|
47 |
case Some(file_model: File_Model) => Some(file_model) |
|
48 |
case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) |
|
49 |
case _ => None |
|
50 |
} |
|
51 |
val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) |
|
52 |
(buffer_model, |
|
53 |
copy(models = models + (node_name -> buffer_model), |
|
54 |
buffer_models = buffer_models + (buffer -> buffer_model))) |
|
55 |
} |
|
56 |
||
57 |
def close_buffer(buffer: JEditBuffer): State = |
|
58 |
{ |
|
59 |
buffer_models.get(buffer) match { |
|
60 |
case None => this |
|
61 |
case Some(buffer_model) => |
|
62 |
val file_model = buffer_model.exit() |
|
63 |
copy(models = models + (file_model.node_name -> file_model), |
|
64 |
buffer_models = buffer_models - buffer) |
|
65 |
} |
|
66 |
} |
|
67 |
} |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
68 |
|
64817 | 69 |
private val state = Synchronized(State()) // owned by GUI thread |
70 |
||
71 |
def get(name: Document.Node.Name): Option[Document_Model] = |
|
72 |
state.value.models.get(name) |
|
73 |
||
74 |
def get(buffer: JEditBuffer): Option[Buffer_Model] = |
|
64813 | 75 |
state.value.buffer_models.get(buffer) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
76 |
|
64817 | 77 |
def is_stable(): Boolean = |
78 |
state.value.models_iterator.forall(_.is_stable) |
|
79 |
||
64831 | 80 |
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = |
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
81 |
for { |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
82 |
model <- state.value.models_iterator |
64831 | 83 |
Text.Info(range, entry) <- model.bibtex_entries |
84 |
} yield Text.Info(range, (entry, model)) |
|
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
85 |
|
64817 | 86 |
|
87 |
/* init and exit */ |
|
88 |
||
89 |
def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = |
|
90 |
{ |
|
91 |
GUI_Thread.require {} |
|
92 |
state.change_result(st => |
|
93 |
st.buffer_models.get(buffer) match { |
|
94 |
case Some(buffer_model) if buffer_model.node_name == node_name => |
|
95 |
buffer_model.init_token_marker |
|
96 |
(buffer_model, st) |
|
97 |
case _ => |
|
98 |
val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) |
|
99 |
buffer.propertiesChanged |
|
100 |
res |
|
101 |
}) |
|
102 |
} |
|
103 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
104 |
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
|
105 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
106 |
GUI_Thread.require {} |
64813 | 107 |
state.change(st => |
64817 | 108 |
if (st.buffer_models.isDefinedAt(buffer)) { |
109 |
val res = st.close_buffer(buffer) |
|
110 |
buffer.propertiesChanged |
|
111 |
res |
|
112 |
} |
|
113 |
else st) |
|
114 |
} |
|
115 |
||
116 |
||
117 |
/* required nodes */ |
|
118 |
||
119 |
def required_nodes(): Set[Document.Node.Name] = |
|
120 |
(for { |
|
121 |
model <- state.value.models_iterator |
|
122 |
if model.node_required |
|
123 |
} yield model.node_name).toSet |
|
124 |
||
125 |
def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false) |
|
126 |
{ |
|
127 |
GUI_Thread.require {} |
|
128 |
||
129 |
val changed = |
|
130 |
state.change_result(st => |
|
131 |
st.models.get(name) match { |
|
132 |
case None => (false, st) |
|
133 |
case Some(model) => |
|
134 |
val required = if (toggle) !model.node_required else set |
|
135 |
model match { |
|
136 |
case model1: File_Model if required != model1.node_required => |
|
137 |
(true, st.copy(models = st.models + (name -> model1.copy(node_required = required)))) |
|
138 |
case model1: Buffer_Model if required != model1.node_required => |
|
139 |
model1.set_node_required(required); (true, st) |
|
140 |
case _ => (false, st) |
|
141 |
} |
|
142 |
}) |
|
143 |
if (changed) { |
|
144 |
PIDE.options_changed() |
|
145 |
PIDE.editor.flush() |
|
146 |
} |
|
147 |
} |
|
148 |
||
149 |
def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit = |
|
150 |
Document_Model.get(view.getBuffer).foreach(model => |
|
151 |
node_required(model.node_name, toggle = toggle, set = set)) |
|
152 |
||
153 |
||
154 |
/* flushed edits */ |
|
155 |
||
156 |
def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) = |
|
157 |
{ |
|
158 |
GUI_Thread.require {} |
|
159 |
||
160 |
state.change_result(st => |
|
161 |
{ |
|
162 |
val doc_blobs = |
|
163 |
Document.Blobs( |
|
164 |
(for { |
|
165 |
model <- st.models_iterator |
|
166 |
blob <- model.get_blob |
|
167 |
} yield (model.node_name -> blob)).toMap) |
|
168 |
||
169 |
val buffer_edits = |
|
170 |
(for { |
|
171 |
model <- st.buffer_models_iterator |
|
172 |
edit <- model.flush_edits(doc_blobs, hidden).iterator |
|
173 |
} yield edit).toList |
|
174 |
||
175 |
val file_edits = |
|
176 |
(for { |
|
177 |
model <- st.file_models_iterator |
|
178 |
change <- model.flush_edits(doc_blobs, hidden) |
|
179 |
} yield change).toList |
|
180 |
||
181 |
val edits = buffer_edits ::: file_edits.flatMap(_._1) |
|
182 |
||
183 |
((doc_blobs, edits), |
|
184 |
st.copy( |
|
185 |
models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) })) |
|
64813 | 186 |
}) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
187 |
} |
43397 | 188 |
|
64817 | 189 |
|
190 |
/* file content */ |
|
191 |
||
192 |
sealed case class File_Content(text: String) |
|
193 |
{ |
|
194 |
lazy val bytes: Bytes = Bytes(text) |
|
195 |
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) |
|
64831 | 196 |
lazy val bibtex_entries: List[Text.Info[String]] = |
197 |
try { Bibtex.document_entries(text) } |
|
64828 | 198 |
catch { case ERROR(msg) => Output.warning(msg); Nil } |
64817 | 199 |
} |
200 |
} |
|
201 |
||
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
202 |
sealed abstract class Document_Model extends Document.Model |
64817 | 203 |
{ |
204 |
/* content */ |
|
205 |
||
64831 | 206 |
def bibtex_entries: List[Text.Info[String]] |
64817 | 207 |
|
208 |
||
209 |
/* perspective */ |
|
210 |
||
211 |
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil |
|
212 |
||
213 |
def node_perspective( |
|
214 |
doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) = |
|
43397 | 215 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
216 |
GUI_Thread.require {} |
64817 | 217 |
|
218 |
if (Isabelle.continuous_checking && is_theory) { |
|
219 |
val snapshot = this.snapshot() |
|
220 |
||
221 |
val reparse = snapshot.node.load_commands_changed(doc_blobs) |
|
222 |
val perspective = |
|
223 |
if (hidden) Text.Perspective.empty |
|
224 |
else { |
|
225 |
val view_ranges = document_view_ranges(snapshot) |
|
226 |
val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) |
|
227 |
Text.Perspective(view_ranges ::: load_ranges) |
|
228 |
} |
|
229 |
val overlays = PIDE.editor.node_overlays(node_name) |
|
230 |
||
231 |
(reparse, Document.Node.Perspective(node_required, perspective, overlays)) |
|
232 |
} |
|
233 |
else (false, Document.Node.no_perspective_text) |
|
43397 | 234 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
235 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
236 |
|
64817 | 237 |
case class File_Model( |
238 |
session: Session, |
|
239 |
node_name: Document.Node.Name, |
|
240 |
content: Document_Model.File_Content, |
|
241 |
node_required: Boolean = false, |
|
242 |
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
|
243 |
pending_edits: List[Text.Edit] = Nil) extends Document_Model |
|
34588 | 244 |
{ |
64817 | 245 |
/* header */ |
246 |
||
247 |
def node_header: Document.Node.Header = |
|
248 |
PIDE.resources.special_header(node_name) getOrElse |
|
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
249 |
PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false) |
64817 | 250 |
|
251 |
||
252 |
/* content */ |
|
253 |
||
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
254 |
def node_position(offset: Text.Offset): Line.Node_Position = |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
255 |
Line.Node_Position(node_name.node, |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
256 |
Line.Position.zero.advance(content.text.substring(0, offset), Text.Length)) |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
257 |
|
64817 | 258 |
def get_blob: Option[Document.Blob] = |
259 |
if (is_theory) None |
|
260 |
else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)) |
|
261 |
||
64831 | 262 |
def bibtex_entries: List[Text.Info[String]] = |
64828 | 263 |
if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil |
64680 | 264 |
|
265 |
||
64817 | 266 |
/* edits */ |
267 |
||
268 |
def update_text(text: String): Option[File_Model] = |
|
269 |
Text.Edit.replace(0, content.text, text) match { |
|
270 |
case Nil => None |
|
271 |
case edits => |
|
272 |
val content1 = Document_Model.File_Content(text) |
|
273 |
val pending_edits1 = pending_edits ::: edits |
|
274 |
Some(copy(content = content1, pending_edits = pending_edits1)) |
|
275 |
} |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
276 |
|
64817 | 277 |
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean) |
278 |
: Option[(List[Document.Edit_Text], File_Model)] = |
|
279 |
{ |
|
280 |
val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
|
281 |
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { |
|
64827
4ef1eb75f1cd
uniform Document.Model.node_edits (without void edits);
wenzelm
parents:
64826
diff
changeset
|
282 |
val edits = node_edits(pending_edits, perspective) |
64817 | 283 |
Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) |
284 |
} |
|
285 |
else None |
|
286 |
} |
|
287 |
||
288 |
||
289 |
/* snapshot */ |
|
290 |
||
291 |
def is_stable: Boolean = pending_edits.isEmpty |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
292 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) |
64817 | 293 |
} |
294 |
||
295 |
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) |
|
296 |
extends Document_Model |
|
297 |
{ |
|
298 |
/* header */ |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
299 |
|
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
300 |
def node_header(): Document.Node.Header = |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
301 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
302 |
GUI_Thread.require {} |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
303 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
63446
diff
changeset
|
304 |
PIDE.resources.special_header(node_name) getOrElse |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
305 |
JEdit_Lib.buffer_lock(buffer) { |
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
306 |
PIDE.resources.check_thy_reader( |
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
307 |
"", node_name, JEdit_Lib.buffer_reader(buffer), strict = false) |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
308 |
} |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
309 |
} |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
310 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
311 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
312 |
/* perspective */ |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
313 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
314 |
// owned by GUI thread |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
315 |
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
|
316 |
def node_required: Boolean = _node_required |
64817 | 317 |
def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } } |
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52807
diff
changeset
|
318 |
|
64817 | 319 |
override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
320 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
321 |
GUI_Thread.require {} |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
322 |
|
64817 | 323 |
(for { |
324 |
doc_view <- PIDE.document_views(buffer).iterator |
|
325 |
range <- doc_view.perspective(snapshot).ranges.iterator |
|
326 |
} yield range).toList |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
327 |
} |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
328 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
329 |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
330 |
/* blob */ |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
331 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
332 |
private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by GUI thread |
54511 | 333 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
334 |
private def reset_blob(): Unit = GUI_Thread.require { _blob = None } |
54511 | 335 |
|
64817 | 336 |
def get_blob: Option[Document.Blob] = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
337 |
GUI_Thread.require { |
55783 | 338 |
if (is_theory) None |
339 |
else { |
|
56473 | 340 |
val (bytes, chunk) = |
55783 | 341 |
_blob match { |
342 |
case Some(x) => x |
|
343 |
case None => |
|
56208 | 344 |
val bytes = PIDE.resources.file_content(buffer) |
56746 | 345 |
val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength)) |
56473 | 346 |
_blob = Some((bytes, chunk)) |
347 |
(bytes, chunk) |
|
55783 | 348 |
} |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
349 |
val changed = pending_edits.nonEmpty |
56473 | 350 |
Some(Document.Blob(bytes, chunk, changed)) |
54511 | 351 |
} |
352 |
} |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
353 |
|
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
354 |
|
58543 | 355 |
/* bibtex entries */ |
356 |
||
64831 | 357 |
private var _bibtex_entries: Option[List[Text.Info[String]]] = None // owned by GUI thread |
58543 | 358 |
|
64817 | 359 |
private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } |
58543 | 360 |
|
64831 | 361 |
def bibtex_entries: List[Text.Info[String]] = |
58543 | 362 |
GUI_Thread.require { |
64828 | 363 |
if (Bibtex.check_name(node_name)) { |
64817 | 364 |
_bibtex_entries match { |
58543 | 365 |
case Some(entries) => entries |
366 |
case None => |
|
64817 | 367 |
val text = JEdit_Lib.buffer_text(buffer) |
64828 | 368 |
val entries = |
64831 | 369 |
try { Bibtex.document_entries(text) } |
64828 | 370 |
catch { case ERROR(msg) => Output.warning(msg); Nil } |
64817 | 371 |
_bibtex_entries = Some(entries) |
58543 | 372 |
entries |
373 |
} |
|
374 |
} |
|
375 |
else Nil |
|
376 |
} |
|
377 |
||
378 |
||
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
|
379 |
/* pending edits */ |
43648 | 380 |
|
60272
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59737
diff
changeset
|
381 |
private object pending_edits |
38224 | 382 |
{ |
38425 | 383 |
private val pending = new mutable.ListBuffer[Text.Edit] |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
57612
diff
changeset
|
384 |
private var last_perspective = Document.Node.no_perspective_text |
44438 | 385 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
386 |
def nonEmpty: Boolean = synchronized { pending.nonEmpty } |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
387 |
def get_edits: List[Text.Edit] = synchronized { pending.toList } |
64817 | 388 |
def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective } |
389 |
def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit = |
|
390 |
synchronized { last_perspective = perspective } |
|
38224 | 391 |
|
64817 | 392 |
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
393 |
synchronized { |
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
394 |
GUI_Thread.require {} |
60272
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59737
diff
changeset
|
395 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
396 |
val edits = get_edits |
64817 | 397 |
val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
398 |
if (reparse || edits.nonEmpty || last_perspective != perspective) { |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
399 |
pending.clear |
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
400 |
last_perspective = perspective |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
401 |
node_edits(edits, perspective) |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
402 |
} |
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
403 |
else Nil |
43648 | 404 |
} |
38224 | 405 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
406 |
def edit(edits: List[Text.Edit]): Unit = synchronized |
38224 | 407 |
{ |
60272
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59737
diff
changeset
|
408 |
GUI_Thread.require {} |
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59737
diff
changeset
|
409 |
|
54511 | 410 |
reset_blob() |
64817 | 411 |
reset_bibtex_entries() |
54511 | 412 |
|
61538
bf4969660913
avoid highlighted area getting "stuck" after edit;
wenzelm
parents:
61192
diff
changeset
|
413 |
for (doc_view <- PIDE.document_views(buffer)) |
bf4969660913
avoid highlighted area getting "stuck" after edit;
wenzelm
parents:
61192
diff
changeset
|
414 |
doc_view.rich_text_area.active_reset() |
bf4969660913
avoid highlighted area getting "stuck" after edit;
wenzelm
parents:
61192
diff
changeset
|
415 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
416 |
pending ++= edits |
54461 | 417 |
PIDE.editor.invoke() |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
418 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
419 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
420 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
421 |
def is_stable(): Boolean = !pending_edits.nonEmpty |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
422 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) |
60933
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60274
diff
changeset
|
423 |
|
64817 | 424 |
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = |
425 |
pending_edits.flush_edits(doc_blobs, hidden) |
|
34828 | 426 |
|
427 |
||
428 |
/* buffer listener */ |
|
429 |
||
430 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
431 |
{ |
|
432 |
override def contentInserted(buffer: JEditBuffer, |
|
433 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
434 |
{ |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
435 |
pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) |
34828 | 436 |
} |
437 |
||
438 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 439 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 440 |
{ |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
441 |
pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) |
34828 | 442 |
} |
443 |
} |
|
444 |
||
445 |
||
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
446 |
/* syntax */ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
447 |
|
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
448 |
def syntax_changed() |
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
449 |
{ |
61192 | 450 |
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) |
59080
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
59079
diff
changeset
|
451 |
for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) |
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
59079
diff
changeset
|
452 |
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). |
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
59079
diff
changeset
|
453 |
invoke(text_area) |
62246
d9410066dbd5
more thorough syntax_changed: new commands need require new folds;
wenzelm
parents:
61728
diff
changeset
|
454 |
buffer.invalidateCachedFoldLevels |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
455 |
} |
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
456 |
|
64817 | 457 |
def init_token_marker() |
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
458 |
{ |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
459 |
Isabelle.buffer_token_marker(buffer) match { |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
460 |
case Some(marker) if marker != buffer.getTokenMarker => |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
461 |
buffer.setTokenMarker(marker) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
462 |
syntax_changed() |
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
463 |
case _ => |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
464 |
} |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
465 |
} |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
466 |
|
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
467 |
|
64817 | 468 |
/* init */ |
469 |
||
470 |
def init(old_model: Option[File_Model]): Buffer_Model = |
|
471 |
{ |
|
472 |
GUI_Thread.require {} |
|
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
473 |
|
64817 | 474 |
old_model match { |
475 |
case None => |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
476 |
pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) |
64817 | 477 |
case Some(file_model) => |
478 |
set_node_required(file_model.node_required) |
|
479 |
pending_edits.set_last_perspective(file_model.last_perspective) |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
480 |
pending_edits.edit( |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
481 |
file_model.pending_edits ::: |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
482 |
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) |
64817 | 483 |
} |
484 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
485 |
buffer.addBufferListener(buffer_listener) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
486 |
init_token_marker() |
64817 | 487 |
|
488 |
this |
|
34680 | 489 |
} |
490 |
||
64817 | 491 |
|
492 |
/* exit */ |
|
493 |
||
494 |
def exit(): File_Model = |
|
34680 | 495 |
{ |
64817 | 496 |
GUI_Thread.require {} |
497 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
498 |
buffer.removeBufferListener(buffer_listener) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
499 |
init_token_marker() |
64817 | 500 |
|
501 |
val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer)) |
|
502 |
File_Model(session, node_name, content, node_required, |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
503 |
pending_edits.get_last_perspective, pending_edits.get_edits) |
34680 | 504 |
} |
34447 | 505 |
} |