--- a/src/Pure/Thy/thy_info.scala Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 17:35:09 2017 +0200
@@ -46,6 +46,7 @@
new Dependencies(rev_entries, keywords, abbrevs, seen + name)
def entries: List[Document.Node.Entry] = rev_entries.reverse
+ def names: List[Document.Node.Name] = entries.map(_.name)
def errors: List[String] = entries.flatMap(_.header.errors)
@@ -57,7 +58,6 @@
def loaded_files: List[(String, List[Path])] =
{
- val names = entries.map(_.name)
names.map(_.theory) zip
Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
}