# HG changeset patch # User wenzelm # Date 1670353731 -3600 # Node ID 6cd6c553b48094b3b47967323e173d193ac98d77 # Parent 127ee77c24ffdd776302ce5cc96d719defa25a06 clarified signature: less redundancy; diff -r 127ee77c24ff -r 6cd6c553b480 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Dec 06 19:29:29 2022 +0100 +++ b/src/Pure/PIDE/resources.scala Tue Dec 06 20:08:51 2022 +0100 @@ -454,4 +454,26 @@ override def toString: String = entries.toString } + + + /* resolve implicit theory dependencies */ + + def resolve_dependencies[A]( + models: Map[A, Document.Model], + theories: List[(Document.Node.Name, Position.T)] + ): List[Document.Node.Name] = { + val model_theories = + (for (model <- models.valuesIterator 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 + thy_name <- make_theory_name(model.node_name) + } yield thy_name).toList + + thy_files1 ::: thy_files2 + } } diff -r 127ee77c24ff -r 6cd6c553b480 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 06 19:29:29 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 06 20:08:51 2022 +0100 @@ -208,26 +208,12 @@ file_watcher: File_Watcher ): (Boolean, Boolean) = { state.change_result { st => - /* theory files */ - - val thys = - (for ((_, model) <- st.models.iterator if model.is_theory) - yield (model.node_name, Position.none)).toList - - val thy_files1 = resources.dependencies(thys).theories - - val thy_files2 = - (for { - (_, model) <- st.models.iterator - thy_name <- resources.make_theory_name(model.node_name) - } yield thy_name).toList - - - /* auxiliary files */ + val thy_files = resources.resolve_dependencies(st.models, Nil) val stable_tip_version = - if (st.models.forall(entry => entry._2.is_stable)) + if (st.models.valuesIterator.forall(_.is_stable)) { session.get_state().stable_tip_version + } else None val aux_files = @@ -236,12 +222,9 @@ case None => Nil } - - /* loaded models */ - val loaded_models = (for { - node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator + node_name <- thy_files.iterator ++ aux_files.iterator file = node_file(node_name) if !st.models.isDefinedAt(file) text <- { file_watcher.register_parent(file); read_file_content(node_name) } diff -r 127ee77c24ff -r 6cd6c553b480 src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Tue Dec 06 19:29:29 2022 +0100 +++ b/src/Tools/jEdit/src/main_plugin.scala Tue Dec 06 20:08:51 2022 +0100 @@ -114,21 +114,12 @@ val required_files = { val models = Document_Model.get_models() - val thys = - (for ((node_name, model) <- models.iterator if model.is_theory) - yield (node_name, Position.none)).toList - val thy_files1 = resources.dependencies(thys).theories - - val thy_files2 = - (for { - (node_name, _) <- models.iterator - thy_name <- resources.make_theory_name(node_name) - } yield thy_name).toList + val thy_files = resources.resolve_dependencies(models, Nil) val aux_files = if (options.bool("jedit_auto_resolve")) { val stable_tip_version = - if (models.forall(p => p._2.is_stable)) { + if (models.valuesIterator.forall(_.is_stable)) { session.get_state().stable_tip_version } else None @@ -139,7 +130,7 @@ } else Nil - (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt) + (thy_files ::: aux_files).filterNot(models.isDefinedAt) } if (required_files.nonEmpty) { try {