# HG changeset patch
# User wenzelm
# Date 1672064697 -3600
# Node ID 7cf9386666418b4bc20af16a0f21af17e2d739ba
# Parent  011759a7f2f68a80383f29731d5946a3271cc713
tuned signature;

diff -r 011759a7f2f6 -r 7cf938666641 src/Tools/VSCode/src/vscode_rendering.scala
--- 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 */
diff -r 011759a7f2f6 -r 7cf938666641 src/Tools/VSCode/src/vscode_resources.scala
--- 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)
diff -r 011759a7f2f6 -r 7cf938666641 src/Tools/jEdit/src/document_model.scala
--- 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 */
diff -r 011759a7f2f6 -r 7cf938666641 src/Tools/jEdit/src/main_plugin.scala
--- 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 {