author | wenzelm |
Tue, 27 Dec 2022 16:36:00 +0100 | |
changeset 76791 | c36d666ee5ee |
parent 76790 | 7a0438979e85 |
child 76792 | 23f433294173 |
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 |
||
64858 | 14 |
import java.io.{File => JFile} |
15 |
||
34693 | 16 |
import scala.collection.mutable |
66019 | 17 |
import scala.annotation.tailrec |
34446 | 18 |
|
72960 | 19 |
import org.gjt.sp.jedit.View |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
20 |
import org.gjt.sp.jedit.Buffer |
61192 | 21 |
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
|
22 |
|
34760 | 23 |
|
75393 | 24 |
object Document_Model { |
64817 | 25 |
/* document models */ |
26 |
||
27 |
sealed case class State( |
|
28 |
models: Map[Document.Node.Name, Document_Model] = Map.empty, |
|
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
29 |
buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty, |
75393 | 30 |
overlays: Document.Overlays = Document.Overlays.empty |
31 |
) { |
|
64868 | 32 |
def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = |
64817 | 33 |
for { |
64868 | 34 |
(node_name, model) <- models.iterator |
76789 | 35 |
file_model <- Library.as_subclass(classOf[File_Model])(model) |
36 |
} yield (node_name, file_model) |
|
64813 | 37 |
|
68476 | 38 |
def document_blobs: Document.Blobs = |
39 |
Document.Blobs( |
|
40 |
(for { |
|
41 |
(node_name, model) <- models.iterator |
|
42 |
blob <- model.get_blob |
|
43 |
} yield (node_name -> blob)).toMap) |
|
44 |
||
75393 | 45 |
def open_buffer( |
46 |
session: Session, |
|
47 |
node_name: Document.Node.Name, |
|
48 |
buffer: Buffer |
|
49 |
) : (Buffer_Model, State) = { |
|
64817 | 50 |
val old_model = |
51 |
models.get(node_name) match { |
|
52 |
case Some(file_model: File_Model) => Some(file_model) |
|
53 |
case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) |
|
54 |
case _ => None |
|
55 |
} |
|
76790
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
56 |
val buffer_model = Buffer_Model.init(old_model, session, node_name, buffer) |
64817 | 57 |
(buffer_model, |
58 |
copy(models = models + (node_name -> buffer_model), |
|
59 |
buffer_models = buffer_models + (buffer -> buffer_model))) |
|
60 |
} |
|
61 |
||
75393 | 62 |
def close_buffer(buffer: JEditBuffer): State = { |
64817 | 63 |
buffer_models.get(buffer) match { |
64 |
case None => this |
|
65 |
case Some(buffer_model) => |
|
66 |
val file_model = buffer_model.exit() |
|
67 |
copy(models = models + (file_model.node_name -> file_model), |
|
68 |
buffer_models = buffer_models - buffer) |
|
69 |
} |
|
70 |
} |
|
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
71 |
|
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
72 |
def provide_file(session: Session, node_name: Document.Node.Name, text: String): State = |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
73 |
if (models.isDefinedAt(node_name)) this |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
74 |
else { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
75 |
val edit = Text.Edit.insert(0, text) |
76783 | 76 |
val content = File_Content(node_name, text) |
77 |
val model = File_Model.init(session, content = content, pending_edits = List(edit)) |
|
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
78 |
copy(models = models + (node_name -> model)) |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
79 |
} |
64817 | 80 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
81 |
|
64817 | 82 |
private val state = Synchronized(State()) // owned by GUI thread |
83 |
||
73999
6b213c0115f5
clarified global state: allow to deactivate main plugin;
wenzelm
parents:
73702
diff
changeset
|
84 |
def reset(): Unit = state.change(_ => State()) |
6b213c0115f5
clarified global state: allow to deactivate main plugin;
wenzelm
parents:
73702
diff
changeset
|
85 |
|
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
86 |
def document_blobs(): Document.Blobs = state.value.document_blobs |
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
87 |
|
76777 | 88 |
def get_models_map(): Map[Document.Node.Name, Document_Model] = state.value.models |
89 |
def get_models(): Iterable[Document_Model] = get_models_map().values |
|
90 |
def get_model(name: Document.Node.Name): Option[Document_Model] = get_models_map().get(name) |
|
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
91 |
def get_model(buffer: JEditBuffer): Option[Buffer_Model] = |
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
92 |
state.value.buffer_models.get(buffer) |
64817 | 93 |
|
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
94 |
def snapshot(model: Document_Model): Document.Snapshot = |
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
95 |
PIDE.session.snapshot( |
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
96 |
node_name = model.node_name, |
76777 | 97 |
pending_edits = Document.Pending_Edits.make(get_models())) |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
98 |
|
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
99 |
def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get_model(name).map(snapshot) |
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
100 |
def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot) |
68476 | 101 |
|
66152 | 102 |
|
103 |
/* bibtex */ |
|
104 |
||
64831 | 105 |
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = |
76777 | 106 |
Bibtex.Entries.iterator(get_models()) |
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
107 |
|
66152 | 108 |
def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset) |
109 |
: Option[Completion.Result] = |
|
76777 | 110 |
Bibtex.completion(history, rendering, caret, get_models()) |
66152 | 111 |
|
64817 | 112 |
|
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
113 |
/* overlays */ |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
114 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
115 |
def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
116 |
state.value.overlays(name) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
117 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
118 |
def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
119 |
state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args))) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
120 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
121 |
def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
122 |
state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args))) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
123 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66082
diff
changeset
|
124 |
|
64858 | 125 |
/* sync external files */ |
126 |
||
75393 | 127 |
def sync_files(changed_files: Set[JFile]): Boolean = { |
75394 | 128 |
state.change_result { st => |
75393 | 129 |
val changed_models = |
130 |
(for { |
|
131 |
(node_name, model) <- st.file_models_iterator |
|
132 |
file <- model.file if changed_files(file) |
|
133 |
text <- PIDE.resources.read_file_content(node_name) |
|
134 |
if model.content.text != text |
|
135 |
} yield { |
|
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
136 |
val content = Document_Model.File_Content(node_name, text) |
75393 | 137 |
val edits = Text.Edit.replace(0, model.content.text, text) |
138 |
(node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits)) |
|
139 |
}).toList |
|
140 |
if (changed_models.isEmpty) (false, st) |
|
141 |
else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _))) |
|
75394 | 142 |
} |
64858 | 143 |
} |
144 |
||
145 |
||
64836 | 146 |
/* syntax */ |
147 |
||
75393 | 148 |
def syntax_changed(names: List[Document.Node.Name]): Unit = { |
64836 | 149 |
GUI_Thread.require {} |
150 |
||
151 |
val models = state.value.models |
|
152 |
for (name <- names.iterator; model <- models.get(name)) { |
|
153 |
model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => } |
|
154 |
} |
|
155 |
} |
|
156 |
||
157 |
||
64817 | 158 |
/* init and exit */ |
159 |
||
75393 | 160 |
def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = { |
64817 | 161 |
GUI_Thread.require {} |
162 |
state.change_result(st => |
|
163 |
st.buffer_models.get(buffer) match { |
|
164 |
case Some(buffer_model) if buffer_model.node_name == node_name => |
|
72960 | 165 |
buffer_model.init_token_marker() |
64817 | 166 |
(buffer_model, st) |
167 |
case _ => |
|
168 |
val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) |
|
72960 | 169 |
buffer.propertiesChanged() |
64817 | 170 |
res |
171 |
}) |
|
172 |
} |
|
173 |
||
75393 | 174 |
def exit(buffer: Buffer): Unit = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
175 |
GUI_Thread.require {} |
64813 | 176 |
state.change(st => |
64817 | 177 |
if (st.buffer_models.isDefinedAt(buffer)) { |
178 |
val res = st.close_buffer(buffer) |
|
72960 | 179 |
buffer.propertiesChanged() |
64817 | 180 |
res |
181 |
} |
|
182 |
else st) |
|
183 |
} |
|
184 |
||
75393 | 185 |
def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit = { |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
186 |
GUI_Thread.require {} |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
187 |
state.change(st => |
73358 | 188 |
files.foldLeft(st) { |
189 |
case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) |
|
190 |
}) |
|
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
191 |
} |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
192 |
|
64817 | 193 |
|
194 |
/* required nodes */ |
|
195 |
||
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
196 |
def nodes_required(): Set[Document.Node.Name] = |
64817 | 197 |
(for { |
64868 | 198 |
(node_name, model) <- state.value.models.iterator |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
199 |
if model.node_required |
64868 | 200 |
} yield node_name).toSet |
64817 | 201 |
|
73340 | 202 |
def node_required( |
75393 | 203 |
name: Document.Node.Name, |
204 |
toggle: Boolean = false, |
|
205 |
set: Boolean = false |
|
206 |
) : Unit = { |
|
64817 | 207 |
GUI_Thread.require {} |
208 |
||
209 |
val changed = |
|
210 |
state.change_result(st => |
|
211 |
st.models.get(name) match { |
|
212 |
case None => (false, st) |
|
213 |
case Some(model) => |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
214 |
val a = model.node_required |
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
215 |
val b = if (toggle) !a else set |
64817 | 216 |
model match { |
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
217 |
case m: File_Model if a != b => |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
218 |
(true, st.copy(models = st.models + (name -> m.set_node_required(b)))) |
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
219 |
case m: Buffer_Model if a != b => |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
220 |
m.set_node_required(b); (true, st) |
64817 | 221 |
case _ => (false, st) |
222 |
} |
|
223 |
}) |
|
76706 | 224 |
if (changed) PIDE.editor.state_changed() |
64817 | 225 |
} |
226 |
||
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
227 |
def view_node_required( |
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
228 |
view: View, |
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
229 |
toggle: Boolean = false, |
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
230 |
set: Boolean = false |
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
231 |
): Unit = |
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
232 |
Document_Model.get_model(view.getBuffer).foreach(model => |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
233 |
node_required(model.node_name, toggle = toggle, set = set)) |
64817 | 234 |
|
235 |
||
236 |
/* flushed edits */ |
|
237 |
||
75393 | 238 |
def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = { |
64817 | 239 |
GUI_Thread.require {} |
240 |
||
75394 | 241 |
state.change_result { st => |
75393 | 242 |
val doc_blobs = st.document_blobs |
64817 | 243 |
|
75393 | 244 |
val buffer_edits = |
245 |
(for { |
|
246 |
(_, model) <- st.buffer_models.iterator |
|
247 |
edit <- model.flush_edits(doc_blobs, hidden).iterator |
|
248 |
} yield edit).toList |
|
64817 | 249 |
|
75393 | 250 |
val file_edits = |
251 |
(for { |
|
252 |
(node_name, model) <- st.file_models_iterator |
|
253 |
(edits, model1) <- model.flush_edits(doc_blobs, hidden) |
|
254 |
} yield (edits, node_name -> model1)).toList |
|
64867 | 255 |
|
75393 | 256 |
val model_edits = buffer_edits ::: file_edits.flatMap(_._1) |
64867 | 257 |
|
75393 | 258 |
val purge_edits = |
259 |
if (purge) { |
|
260 |
val purged = |
|
261 |
(for ((node_name, model) <- st.file_models_iterator) |
|
262 |
yield (node_name -> model.purge_edits(doc_blobs))).toList |
|
64817 | 263 |
|
75393 | 264 |
val imports = { |
265 |
val open_nodes = |
|
266 |
(for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList |
|
267 |
val touched_nodes = model_edits.map(_._1) |
|
268 |
val pending_nodes = for ((node_name, None) <- purged) yield node_name |
|
269 |
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) |
|
270 |
} |
|
271 |
val retain = PIDE.resources.dependencies(imports).theories.toSet |
|
64817 | 272 |
|
75393 | 273 |
for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits) |
274 |
yield edit |
|
275 |
} |
|
276 |
else Nil |
|
64867 | 277 |
|
75393 | 278 |
val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1)) |
279 |
PIDE.plugin.file_watcher.purge( |
|
280 |
(for { |
|
281 |
(_, model) <- st1.file_models_iterator |
|
282 |
file <- model.file |
|
283 |
} yield file.getParentFile).toSet) |
|
64867 | 284 |
|
75393 | 285 |
((doc_blobs, model_edits ::: purge_edits), st1) |
75394 | 286 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
287 |
} |
43397 | 288 |
|
64817 | 289 |
|
290 |
/* file content */ |
|
291 |
||
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
292 |
object File_Content { |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
293 |
val empty: File_Content = apply(Document.Node.Name.empty, "") |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
294 |
|
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
295 |
def apply(node_name: Document.Node.Name, text: String): File_Content = |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
296 |
new File_Content(node_name, text) |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
297 |
} |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
298 |
|
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
299 |
final class File_Content private(val node_name: Document.Node.Name, val text: String) { |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
300 |
override def toString: String = "Document_Model.File_Content(" + node_name.node + ")" |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64832
diff
changeset
|
301 |
lazy val bytes: Bytes = Bytes(Symbol.encode(text)) |
64817 | 302 |
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) |
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
303 |
lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node) |
64817 | 304 |
} |
66019 | 305 |
|
306 |
||
307 |
/* HTTP preview */ |
|
308 |
||
75393 | 309 |
def open_preview(view: View, plain_text: Boolean): Unit = { |
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
310 |
Document_Model.get_model(view.getBuffer) match { |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67244
diff
changeset
|
311 |
case Some(model) => |
75148 | 312 |
val url = Preview_Service.server_url(plain_text, model.node_name) |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67244
diff
changeset
|
313 |
PIDE.editor.hyperlink_url(url).follow(view) |
66036 | 314 |
case _ => |
66019 | 315 |
} |
316 |
} |
|
317 |
||
75393 | 318 |
object Preview_Service extends HTTP.Service("preview") { |
75148 | 319 |
service => |
320 |
||
321 |
private val plain_text_prefix = "plain_text=" |
|
322 |
||
323 |
def server_url(plain_text: Boolean, node_name: Document.Node.Name): String = |
|
324 |
PIDE.plugin.http_server.url + "/" + service.name + "?" + |
|
325 |
(if (plain_text) plain_text_prefix else "") + Url.encode(node_name.node) |
|
326 |
||
75113 | 327 |
def apply(request: HTTP.Request): Option[HTTP.Response] = |
75107 | 328 |
for { |
75112 | 329 |
query <- request.decode_query |
75107 | 330 |
name = Library.perhaps_unprefix(plain_text_prefix, query) |
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
331 |
model <- get_model(PIDE.resources.node_name(name)) |
75107 | 332 |
} |
333 |
yield { |
|
334 |
val snapshot = model.await_stable_snapshot() |
|
75979 | 335 |
val context = |
336 |
Browser_Info.context(PIDE.resources.sessions_structure, |
|
337 |
elements = Browser_Info.extra_elements) |
|
75107 | 338 |
val document = |
75979 | 339 |
context.preview_document(snapshot, |
75107 | 340 |
plain_text = query.startsWith(plain_text_prefix), |
75146 | 341 |
fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name))) |
75107 | 342 |
HTTP.Response.html(document.content) |
75113 | 343 |
} |
344 |
} |
|
64817 | 345 |
} |
346 |
||
75393 | 347 |
sealed abstract class Document_Model extends Document.Model { |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
348 |
model => |
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
349 |
|
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
350 |
|
64817 | 351 |
/* perspective */ |
352 |
||
353 |
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil |
|
354 |
||
355 |
def node_perspective( |
|
75393 | 356 |
doc_blobs: Document.Blobs, |
357 |
hidden: Boolean |
|
76702 | 358 |
): (Boolean, Document.Node.Perspective_Text.T) = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
359 |
GUI_Thread.require {} |
64817 | 360 |
|
75849 | 361 |
if (JEdit_Options.continuous_checking() && is_theory) { |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
362 |
val snapshot = Document_Model.snapshot(model) |
64817 | 363 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
364 |
val required = node_required || PIDE.editor.document_node_required(node_name) |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
365 |
|
64817 | 366 |
val reparse = snapshot.node.load_commands_changed(doc_blobs) |
367 |
val perspective = |
|
368 |
if (hidden) Text.Perspective.empty |
|
369 |
else { |
|
370 |
val view_ranges = document_view_ranges(snapshot) |
|
71601 | 371 |
val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node) |
64817 | 372 |
Text.Perspective(view_ranges ::: load_ranges) |
373 |
} |
|
66082 | 374 |
val overlays = PIDE.editor.node_overlays(node_name) |
64817 | 375 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
376 |
(reparse, Document.Node.Perspective(required, perspective, overlays)) |
64817 | 377 |
} |
76702 | 378 |
else (false, Document.Node.Perspective_Text.empty) |
43397 | 379 |
} |
66019 | 380 |
|
381 |
||
382 |
/* snapshot */ |
|
383 |
||
75393 | 384 |
@tailrec final def await_stable_snapshot(): Document.Snapshot = { |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
385 |
val snapshot = Document_Model.snapshot(model) |
66019 | 386 |
if (snapshot.is_outdated) { |
76610 | 387 |
PIDE.session.output_delay.sleep() |
66019 | 388 |
await_stable_snapshot() |
389 |
} |
|
390 |
else snapshot |
|
391 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
392 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
393 |
|
75393 | 394 |
object File_Model { |
64863 | 395 |
def init(session: Session, |
76783 | 396 |
content: Document_Model.File_Content = Document_Model.File_Content.empty, |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
397 |
node_required: Boolean = false, |
76702 | 398 |
last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty, |
75393 | 399 |
pending_edits: List[Text.Edit] = Nil |
400 |
): File_Model = { |
|
76783 | 401 |
val node_name = content.node_name |
402 |
||
65469 | 403 |
val file = JEdit_Lib.check_file(node_name.node) |
65245 | 404 |
file.foreach(PIDE.plugin.file_watcher.register_parent(_)) |
64863 | 405 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
406 |
val node_required1 = node_required || File_Format.registry.is_theory(node_name) |
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
407 |
File_Model(session, file, content, node_required1, last_perspective, pending_edits) |
64863 | 408 |
} |
409 |
} |
|
410 |
||
64817 | 411 |
case class File_Model( |
412 |
session: Session, |
|
64864
eec7ffef0be6
accomodate very big file_models and changed_files;
wenzelm
parents:
64863
diff
changeset
|
413 |
file: Option[JFile], |
64817 | 414 |
content: Document_Model.File_Content, |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
415 |
node_required: Boolean, |
76702 | 416 |
last_perspective: Document.Node.Perspective_Text.T, |
75393 | 417 |
pending_edits: List[Text.Edit] |
418 |
) extends Document_Model { |
|
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
419 |
/* content */ |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
420 |
|
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
421 |
def node_name: Document.Node.Name = content.node_name |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
422 |
|
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
423 |
def get_text(range: Text.Range): Option[String] = |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
424 |
range.try_substring(content.text) |
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
425 |
|
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
426 |
|
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
427 |
/* required */ |
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
428 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
429 |
def set_node_required(b: Boolean): File_Model = copy(node_required = b) |
76481
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
430 |
|
a9d52d02bd83
clarified node_required status: distinguish theory_required vs. document_required;
wenzelm
parents:
75979
diff
changeset
|
431 |
|
64817 | 432 |
/* header */ |
433 |
||
434 |
def node_header: Document.Node.Header = |
|
435 |
PIDE.resources.special_header(node_name) getOrElse |
|
72772 | 436 |
PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false) |
64817 | 437 |
|
438 |
||
439 |
/* content */ |
|
440 |
||
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
441 |
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
|
442 |
Line.Node_Position(node_name.node, |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65132
diff
changeset
|
443 |
Line.Position.zero.advance(content.text.substring(0, offset))) |
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64828
diff
changeset
|
444 |
|
64817 | 445 |
def get_blob: Option[Document.Blob] = |
446 |
if (is_theory) None |
|
67265
f32287c95432
store full blob source for the sake of markup_to_XML;
wenzelm
parents:
67262
diff
changeset
|
447 |
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) |
64817 | 448 |
|
76776 | 449 |
def bibtex_entries: Bibtex.Entries = |
450 |
if (File.is_bib(node_name.node)) content.bibtex_entries else Bibtex.Entries.empty |
|
64680 | 451 |
|
452 |
||
64817 | 453 |
/* edits */ |
454 |
||
455 |
def update_text(text: String): Option[File_Model] = |
|
456 |
Text.Edit.replace(0, content.text, text) match { |
|
457 |
case Nil => None |
|
458 |
case edits => |
|
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
459 |
val content1 = Document_Model.File_Content(node_name, text) |
64817 | 460 |
val pending_edits1 = pending_edits ::: edits |
461 |
Some(copy(content = content1, pending_edits = pending_edits1)) |
|
462 |
} |
|
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
463 |
|
75393 | 464 |
def flush_edits( |
465 |
doc_blobs: Document.Blobs, |
|
466 |
hidden: Boolean |
|
76607 | 467 |
): Option[(List[Document.Edit_Text], File_Model)] = { |
64817 | 468 |
val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
469 |
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { |
|
64867 | 470 |
val edits = node_edits(node_header, pending_edits, perspective) |
64817 | 471 |
Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) |
472 |
} |
|
473 |
else None |
|
474 |
} |
|
475 |
||
64867 | 476 |
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] = |
67310 | 477 |
if (pending_edits.nonEmpty || |
71733 | 478 |
!File_Format.registry.is_theory(node_name) && |
76702 | 479 |
(node_required || !Document.Node.Perspective_Text.is_empty(last_perspective))) None |
64867 | 480 |
else { |
481 |
val text_edits = List(Text.Edit.remove(0, content.text)) |
|
76702 | 482 |
Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty)) |
64867 | 483 |
} |
484 |
||
64817 | 485 |
def is_stable: Boolean = pending_edits.isEmpty |
486 |
} |
|
487 |
||
76790
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
488 |
object Buffer_Model { |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
489 |
def init( |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
490 |
old_model: Option[File_Model], |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
491 |
session: Session, |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
492 |
node_name: Document.Node.Name, |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
493 |
buffer: Buffer |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
494 |
): Buffer_Model = (new Buffer_Model(session, node_name, buffer)).init(old_model) |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
495 |
} |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
496 |
|
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
497 |
class Buffer_Model private( |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
498 |
val session: Session, |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
499 |
val node_name: Document.Node.Name, |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
500 |
val buffer: Buffer |
7a0438979e85
clarified signature: avoid case class with mutable state;
wenzelm
parents:
76789
diff
changeset
|
501 |
) extends Document_Model { |
66114 | 502 |
/* text */ |
503 |
||
67014 | 504 |
def get_text(range: Text.Range): Option[String] = |
505 |
JEdit_Lib.get_text(buffer, range) |
|
66114 | 506 |
|
507 |
||
64817 | 508 |
/* 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
|
509 |
|
75393 | 510 |
def node_header(): Document.Node.Header = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
511 |
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
|
512 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
63446
diff
changeset
|
513 |
PIDE.resources.special_header(node_name) getOrElse |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
514 |
JEdit_Lib.buffer_lock(buffer) { |
72772 | 515 |
PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false) |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
516 |
} |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
517 |
} |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
518 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
519 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
520 |
/* perspective */ |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
521 |
|
64883 | 522 |
def document_view_iterator: Iterator[Document_View] = |
523 |
for { |
|
524 |
text_area <- JEdit_Lib.jedit_text_areas(buffer) |
|
525 |
doc_view <- Document_View.get(text_area) |
|
526 |
} yield doc_view |
|
527 |
||
75393 | 528 |
override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57610
diff
changeset
|
529 |
GUI_Thread.require {} |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
530 |
|
64817 | 531 |
(for { |
64883 | 532 |
doc_view <- document_view_iterator |
64817 | 533 |
range <- doc_view.perspective(snapshot).ranges.iterator |
534 |
} yield range).toList |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
535 |
} |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
536 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
537 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
538 |
/* mutable buffer state: owned by GUI thread */ |
54511 | 539 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
540 |
private object buffer_state { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
541 |
// perspective and edits |
58543 | 542 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
543 |
private var last_perspective = Document.Node.Perspective_Text.empty |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
544 |
def get_last_perspective: Document.Node.Perspective_Text.T = |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
545 |
GUI_Thread.require { last_perspective } |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
546 |
def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit = |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
547 |
GUI_Thread.require { last_perspective = perspective } |
58543 | 548 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
549 |
private var node_required = false |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
550 |
def get_node_required: Boolean = GUI_Thread.require { node_required } |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
551 |
def set_node_required(b: Boolean): Unit = GUI_Thread.require { node_required = b } |
58543 | 552 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
553 |
private val pending_edits = new mutable.ListBuffer[Text.Edit] |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
554 |
def is_stable: Boolean = GUI_Thread.require { pending_edits.isEmpty } |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
555 |
def get_pending_edits: List[Text.Edit] = GUI_Thread.require { pending_edits.toList } |
38224 | 556 |
|
64817 | 557 |
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
558 |
GUI_Thread.require { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
559 |
val edits = get_pending_edits |
64817 | 560 |
val (reparse, perspective) = node_perspective(doc_blobs, hidden) |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
561 |
if (reparse || edits.nonEmpty || last_perspective != perspective) { |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
562 |
pending_edits.clear() |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
563 |
last_perspective = perspective |
71601 | 564 |
node_edits(node_header(), edits, perspective) |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
565 |
} |
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61538
diff
changeset
|
566 |
else Nil |
43648 | 567 |
} |
38224 | 568 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
569 |
def edit(edits: List[Text.Edit]): Unit = GUI_Thread.require { |
54511 | 570 |
reset_blob() |
64817 | 571 |
reset_bibtex_entries() |
54511 | 572 |
|
76762 | 573 |
for (doc_view <- document_view_iterator) { |
61538
bf4969660913
avoid highlighted area getting "stuck" after edit;
wenzelm
parents:
61192
diff
changeset
|
574 |
doc_view.rich_text_area.active_reset() |
76762 | 575 |
} |
61538
bf4969660913
avoid highlighted area getting "stuck" after edit;
wenzelm
parents:
61192
diff
changeset
|
576 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
577 |
pending_edits ++= edits |
66082 | 578 |
PIDE.editor.invoke() |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
579 |
} |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
580 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
581 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
582 |
// blob |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
583 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
584 |
private var blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
585 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
586 |
def reset_blob(): Unit = GUI_Thread.require { blob = None } |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
587 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
588 |
def get_blob: Option[Document.Blob] = GUI_Thread.require { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
589 |
if (is_theory) None |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
590 |
else { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
591 |
val (bytes, text, chunk) = |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
592 |
blob getOrElse { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
593 |
val bytes = PIDE.resources.make_file_content(buffer) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
594 |
val text = buffer.getText(0, buffer.getLength) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
595 |
val chunk = Symbol.Text_Chunk(text) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
596 |
val x = (bytes, text, chunk) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
597 |
blob = Some(x) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
598 |
x |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
599 |
} |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
600 |
val changed = !is_stable |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
601 |
Some(Document.Blob(bytes, text, chunk, changed)) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
602 |
} |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
603 |
} |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
604 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
605 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
606 |
// bibtex entries |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
607 |
|
76776 | 608 |
private var bibtex_entries: Option[Bibtex.Entries] = None |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
609 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
610 |
def reset_bibtex_entries(): Unit = GUI_Thread.require { bibtex_entries = None } |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
611 |
|
76776 | 612 |
def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require { |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
613 |
if (File.is_bib(node_name.node)) { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
614 |
bibtex_entries getOrElse { |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
615 |
val text = JEdit_Lib.buffer_text(buffer) |
76781
d9f48960bf23
clarified signature: more position information via node_name;
wenzelm
parents:
76778
diff
changeset
|
616 |
val entries = Bibtex.Entries.parse(text, file_pos = node_name.node) |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
617 |
bibtex_entries = Some(entries) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
618 |
entries |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
619 |
} |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
620 |
} |
76776 | 621 |
else Bibtex.Entries.empty |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
622 |
} |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
623 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
624 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
625 |
def is_stable: Boolean = buffer_state.is_stable |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
626 |
def pending_edits: List[Text.Edit] = buffer_state.get_pending_edits |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
627 |
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
628 |
buffer_state.flush_edits(doc_blobs, hidden) |
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
|
629 |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
630 |
def node_required: Boolean = buffer_state.get_node_required |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
631 |
def set_node_required(b: Boolean): Unit = buffer_state.set_node_required(b) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
632 |
|
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
633 |
def get_blob: Option[Document.Blob] = buffer_state.get_blob |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
634 |
|
76776 | 635 |
def bibtex_entries: Bibtex.Entries = buffer_state.get_bibtex_entries |
34828 | 636 |
|
637 |
||
638 |
/* buffer listener */ |
|
639 |
||
75393 | 640 |
private val buffer_listener: BufferListener = new BufferAdapter { |
641 |
override def contentInserted( |
|
642 |
buffer: JEditBuffer, |
|
643 |
start_line: Int, |
|
644 |
offset: Int, |
|
645 |
num_lines: Int, |
|
646 |
length: Int |
|
647 |
): Unit = { |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
648 |
buffer_state.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) |
34828 | 649 |
} |
650 |
||
75393 | 651 |
override def preContentRemoved( |
652 |
buffer: JEditBuffer, |
|
653 |
start_line: Int, |
|
654 |
offset: Int, |
|
655 |
num_lines: Int, |
|
656 |
removed_length: Int |
|
657 |
): Unit = { |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
658 |
buffer_state.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) |
34828 | 659 |
} |
660 |
} |
|
661 |
||
662 |
||
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
663 |
/* syntax */ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
664 |
|
75393 | 665 |
def syntax_changed(): Unit = { |
61192 | 666 |
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) |
76762 | 667 |
for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { |
59080
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
59079
diff
changeset
|
668 |
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
|
669 |
invoke(text_area) |
76762 | 670 |
} |
72960 | 671 |
buffer.invalidateCachedFoldLevels() |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
672 |
} |
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
673 |
|
75393 | 674 |
def init_token_marker(): Unit = { |
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
675 |
Isabelle.buffer_token_marker(buffer) match { |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
676 |
case Some(marker) if marker != buffer.getTokenMarker => |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
677 |
buffer.setTokenMarker(marker) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
678 |
syntax_changed() |
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
679 |
case _ => |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
680 |
} |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
681 |
} |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
59076
diff
changeset
|
682 |
|
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
683 |
|
64817 | 684 |
/* init */ |
685 |
||
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
686 |
def init(old_model: Option[File_Model]): Buffer_Model = GUI_Thread.require { |
64817 | 687 |
old_model match { |
688 |
case None => |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
689 |
buffer_state.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) |
64817 | 690 |
case Some(file_model) => |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76706
diff
changeset
|
691 |
set_node_required(file_model.node_required) |
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
692 |
buffer_state.set_last_perspective(file_model.last_perspective) |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
693 |
buffer_state.edit( |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
694 |
file_model.pending_edits ::: |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
695 |
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) |
64817 | 696 |
} |
697 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
698 |
buffer.addBufferListener(buffer_listener) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
699 |
init_token_marker() |
64817 | 700 |
|
701 |
this |
|
34680 | 702 |
} |
703 |
||
64817 | 704 |
|
705 |
/* exit */ |
|
706 |
||
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
707 |
def exit(): File_Model = GUI_Thread.require { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
708 |
buffer.removeBufferListener(buffer_listener) |
59078
cf255dc2b48f
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents:
59077
diff
changeset
|
709 |
init_token_marker() |
64817 | 710 |
|
76783 | 711 |
File_Model.init(session, |
712 |
content = Document_Model.File_Content(node_name, JEdit_Lib.buffer_text(buffer)), |
|
76775
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
713 |
node_required = node_required, |
01a7265db76b
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
wenzelm
parents:
76768
diff
changeset
|
714 |
last_perspective = buffer_state.get_last_perspective, |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
76763
diff
changeset
|
715 |
pending_edits = pending_edits) |
34680 | 716 |
} |
34447 | 717 |
} |