--- a/src/Pure/PIDE/resources.scala Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Dec 23 22:48:29 2022 +0100
@@ -458,18 +458,18 @@
/* resolve implicit theory dependencies */
def resolve_dependencies[A](
- models: Map[A, Document.Model],
+ models: Iterable[Document.Model],
theories: List[(Document.Node.Name, Position.T)]
): List[Document.Node.Name] = {
val model_theories =
- (for (model <- models.valuesIterator if model.is_theory)
+ (for (model <- models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
val thy_files1 = dependencies(model_theories ::: theories).theories
val thy_files2 =
(for {
- model <- models.valuesIterator if !model.is_theory
+ model <- models.iterator if !model.is_theory
thy_name <- make_theory_name(model.node_name)
} yield thy_name).toList
--- a/src/Pure/PIDE/session.scala Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Pure/PIDE/session.scala Fri Dec 23 22:48:29 2022 +0100
@@ -697,8 +697,8 @@
get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
resources.session_base.overall_syntax
- def stable_tip_version[A](models: Map[A, Document.Model]): Option[Document.Version] =
- if (models.forall(p => p._2.pending_edits.isEmpty)) get_state().stable_tip_version
+ def stable_tip_version[A](models: Iterable[Document.Model]): Option[Document.Version] =
+ if (models.forall(model => model.pending_edits.isEmpty)) get_state().stable_tip_version
else None
@tailrec final def await_stable_snapshot(): Document.Snapshot = {
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 23 22:48:29 2022 +0100
@@ -235,10 +235,10 @@
file_watcher: File_Watcher
): (Boolean, Boolean) = {
state.change_result { st =>
- val stable_tip_version = session.stable_tip_version(st.models)
+ val stable_tip_version = session.stable_tip_version(st.models.values)
val thy_files =
- resources.resolve_dependencies(st.models,
+ resources.resolve_dependencies(st.models.values,
editor.document_required().map((_, Position.none)))
val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
--- a/src/Tools/jEdit/src/main_plugin.scala Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Fri Dec 23 22:48:29 2022 +0100
@@ -113,12 +113,12 @@
val models = Document_Model.get_models()
val thy_files =
- resources.resolve_dependencies(models,
+ resources.resolve_dependencies(models.values,
PIDE.editor.document_required().map((_, Position.none)))
val aux_files =
if (resources.auto_resolve) {
- session.stable_tip_version(models) match {
+ session.stable_tip_version(models.values) match {
case Some(version) => resources.undefined_blobs(version)
case None => delay_load.invoke(); Nil
}