--- a/src/Pure/PIDE/resources.scala Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/PIDE/resources.scala Tue Dec 01 16:07:19 2020 +0100
@@ -398,20 +398,17 @@
graph2.map_node(name, _ => syntax)
})
- def loaded_files(pure: Boolean): List[(String, List[Path])] =
+ def loaded_files: List[(String, List[Path])] =
{
- val loaded_files =
- theories.map(_.theory) zip
- Par_List.map((e: () => List[Path]) => e(),
- theories.map(name =>
- resources.loaded_files(loaded_theories.get_node(name.theory), name)))
-
- if (pure) {
- val pure_files = resources.pure_files(overall_syntax)
- loaded_files.map({ case (name, files) =>
- (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
- }
- else loaded_files
+ theories.zip(
+ Par_List.map((e: () => List[Path]) => e(),
+ theories.map(name =>
+ resources.loaded_files(loaded_theories.get_node(name.theory), name))))
+ .map({ case (name, files) =>
+ val files1 =
+ if (name.theory == Thy_Header.PURE) resources.pure_files(overall_syntax) ::: files
+ else files
+ (name.theory, files1) })
}
def imported_files: List[Path] =