--- a/src/Pure/PIDE/headless.scala Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/PIDE/headless.scala Tue Dec 01 16:07:19 2020 +0100
@@ -256,7 +256,7 @@
val dep_theories = dependencies.theories
val dep_theories_set = dep_theories.toSet
val dep_files =
- dependencies.loaded_files(false).flatMap(_._2).
+ dependencies.loaded_files.flatMap(_._2).
map(path => Document.Node.Name(resources.append("", path)))
val use_theories_state =
--- 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] =
--- a/src/Pure/Thy/sessions.scala Mon Nov 30 22:00:23 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Tue Dec 01 16:07:19 2020 +0100
@@ -173,10 +173,7 @@
val theory_files = dependencies.theories.map(_.path)
val (loaded_files, loaded_files_errors) =
- try {
- if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
- else (Nil, Nil)
- }
+ try { if (inlined_files) (dependencies.loaded_files, Nil) else (Nil, Nil) }
catch { case ERROR(msg) => (Nil, List(msg)) }
val session_files =