--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 15:11:42 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 15:24:57 2022 +0100
@@ -78,10 +78,10 @@
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
- Bibtex.Entries.iterator(resources.get_models().values)
+ Bibtex.Entries.iterator(resources.get_models())
def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, resources.get_models().values)
+ Bibtex.completion(history, rendering, caret, resources.get_models())
/* completion */
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 15:11:42 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 15:24:57 2022 +0100
@@ -113,8 +113,8 @@
else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
}
- def get_models(): Map[JFile, VSCode_Model] = state.value.models
- def get_model(file: JFile): Option[VSCode_Model] = get_models().get(file)
+ def get_models(): Iterable[VSCode_Model] = state.value.models.values
+ def get_model(file: JFile): Option[VSCode_Model] = state.value.models.get(file)
def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
@@ -123,7 +123,7 @@
def snapshot(model: VSCode_Model): Document.Snapshot =
model.session.snapshot(
node_name = model.node_name,
- pending_edits = Document.Pending_Edits.make(get_models().values))
+ pending_edits = Document.Pending_Edits.make(get_models()))
def get_snapshot(file: JFile): Option[Document.Snapshot] =
get_model(file).map(snapshot)
--- a/src/Tools/jEdit/src/document_model.scala Mon Dec 26 15:11:42 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 26 15:24:57 2022 +0100
@@ -84,15 +84,16 @@
def document_blobs(): Document.Blobs = state.value.document_blobs
- def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
- def get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
+ def get_models_map(): Map[Document.Node.Name, Document_Model] = state.value.models
+ def get_models(): Iterable[Document_Model] = get_models_map().values
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_models_map().get(name)
def get_model(buffer: JEditBuffer): Option[Buffer_Model] =
state.value.buffer_models.get(buffer)
def snapshot(model: Document_Model): Document.Snapshot =
PIDE.session.snapshot(
node_name = model.node_name,
- pending_edits = Document.Pending_Edits.make(get_models().values))
+ pending_edits = Document.Pending_Edits.make(get_models()))
def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get_model(name).map(snapshot)
def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
@@ -101,11 +102,11 @@
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- Bibtex.Entries.iterator(get_models().values)
+ Bibtex.Entries.iterator(get_models())
def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
: Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, get_models().values)
+ Bibtex.completion(history, rendering, caret, get_models())
/* overlays */
--- a/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 15:11:42 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 15:24:57 2022 +0100
@@ -110,7 +110,7 @@
private def delay_load_body(): Unit = {
val required_files = {
- val models = Document_Model.get_models()
+ val models = Document_Model.get_models_map()
val thy_files =
resources.resolve_dependencies(models.values, PIDE.editor.document_required())
@@ -124,7 +124,7 @@
}
else Nil
- (thy_files ::: aux_files).filterNot(models.isDefinedAt)
+ (thy_files ::: aux_files).filterNot(models.keySet)
}
if (required_files.nonEmpty) {
try {