src/Pure/Thy/thy_info.scala
changeset 66715 6bced18e2b91
parent 66714 9fc4e144693c
child 66717 67dbf5cdc056
--- 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, _)))
     }