# HG changeset patch
# User wenzelm
# Date 1527498917 -7200
# Node ID 09270aa4088476ce709a20a92dd14a857c04cd7f
# Parent  fb5653a7a8790cd7c10f389a82021b4a8a45e3bd
tuned signature;

diff -r fb5653a7a879 -r 09270aa40884 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun May 27 23:15:47 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon May 28 11:15:17 2018 +0200
@@ -679,6 +679,15 @@
       new Structure(restrict(build_graph), restrict(imports_graph))
     }
 
+    def selection_deps(sel: Selection,
+      progress: Progress = No_Progress,
+      inlined_files: Boolean = false,
+      verbose: Boolean = false): Deps =
+    {
+      Sessions.deps(selection(sel), global_theories,
+        progress = progress, inlined_files = inlined_files, verbose = verbose)
+    }
+
     def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
diff -r fb5653a7a879 -r 09270aa40884 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Sun May 27 23:15:47 2018 +0200
+++ b/src/Pure/Tools/imports.scala	Mon May 28 11:15:17 2018 +0200
@@ -99,11 +99,9 @@
     select_dirs: List[Path] = Nil,
     verbose: Boolean = false) =
   {
-    val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
-
     val deps =
-      Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
-        progress = progress, verbose = verbose).check_errors
+      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
+        selection_deps(selection, progress = progress, verbose = verbose).check_errors
 
     val root_keywords = Sessions.root_syntax.keywords