# HG changeset patch
# User wenzelm
# Date 1506699309 -7200
# Node ID 6bced18e2b919b469b3367af00ff671710afc502
# Parent  9fc4e144693c7b6b3aec49014bf775124530a18c
tuned;

diff -r 9fc4e144693c -r 6bced18e2b91 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:35:09 2017 +0200
@@ -205,7 +205,7 @@
 
             val syntax = thy_deps.syntax
 
-            val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node))
+            val theory_files = thy_deps.names.map(name => Path.explode(name.node))
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
@@ -262,7 +262,7 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                theories = thy_deps.entries.map(_.name),
+                theories = thy_deps.names,
                 loaded_files = loaded_files)
 
             val sources =
diff -r 9fc4e144693c -r 6bced18e2b91 src/Pure/Thy/thy_info.scala
--- 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, _)))
     }
diff -r 9fc4e144693c -r 6bced18e2b91 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:35:09 2017 +0200
@@ -216,7 +216,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = thy_info.dependencies(thys).entries.map(_.name)
+        val thy_files = thy_info.dependencies(thys).names
 
 
         /* auxiliary files */
diff -r 9fc4e144693c -r 6bced18e2b91 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:35:09 2017 +0200
@@ -253,7 +253,7 @@
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
-            val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet
+            val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
diff -r 9fc4e144693c -r 6bced18e2b91 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:35:09 2017 +0200
@@ -126,7 +126,7 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.thy_info.dependencies(thys).entries.map(_.name)
+          val thy_files = resources.thy_info.dependencies(thys).names
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {