# HG changeset patch
# User wenzelm
# Date 1510512379 -3600
# Node ID df7d728103f17939b2d6bc78852ca1d945978804
# Parent  03d4954c68bbaff41e15eb15717058f410ef39a0
tuned signature;

diff -r 03d4954c68bb -r df7d728103f1 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -249,7 +249,7 @@
       new Dependencies(rev_entries, seen + name)
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
-    def names: List[Document.Node.Name] = entries.map(_.name)
+    def theories: List[Document.Node.Name] = entries.map(_.name)
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
@@ -276,15 +276,15 @@
 
     def loaded_files: List[(String, List[Path])] =
     {
-      names.map(_.theory) zip
+      theories.map(_.theory) zip
         Par_List.map((e: () => List[Path]) => e(),
-          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+          theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     }
 
     def imported_files: List[Path] =
     {
       val base_theories =
-        loaded_theories.all_preds(names.map(_.theory)).
+        loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined(_))
 
       base_theories.map(theory => session_base.known.theories(theory).path) :::
diff -r 03d4954c68bb -r df7d728103f1 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -234,7 +234,7 @@
 
             val overall_syntax = dependencies.overall_syntax
 
-            val theory_files = dependencies.names.map(_.path)
+            val theory_files = dependencies.theories.map(_.path)
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
@@ -294,7 +294,7 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                theories = dependencies.names,
+                theories = dependencies.theories,
                 loaded_files = loaded_files)
 
             val sources_errors =
diff -r 03d4954c68bb -r df7d728103f1 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -66,7 +66,7 @@
       yield (import_name(qualifier, master_dir, thy), pos)
 
     val dependencies = resources.dependencies(import_names).check_errors
-    val loaded_theories = dependencies.names.map(read_thy(_))
+    val loaded_theories = dependencies.theories.map(read_thy(_))
 
     val edits =
       state.change_result(st =>
@@ -84,6 +84,6 @@
       })
     session.update(Document.Blobs.empty, edits)
 
-    dependencies.names
+    dependencies.theories
   }
 }
diff -r 03d4954c68bb -r df7d728103f1 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -208,7 +208,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = dependencies(thys).names
+        val thy_files = dependencies(thys).theories
 
 
         /* auxiliary files */
diff -r 03d4954c68bb -r df7d728103f1 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -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.dependencies(imports).names.toSet
+            val retain = PIDE.resources.dependencies(imports).theories.toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
diff -r 03d4954c68bb -r df7d728103f1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 12 19:46:19 2017 +0100
@@ -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.dependencies(thys).names
+          val thy_files = resources.dependencies(thys).theories
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {