# HG changeset patch
# User wenzelm
# Date 1546012707 -3600
# Node ID fa94f2b2a8775c310bd190f0f156c9d2a16102ab
# Parent  9403ff523825fda4a4cd428c02d35b16293b9b4a
clarified sessions_deps, according to Isabelle/MMT usage;

diff -r 9403ff523825 -r fa94f2b2a877 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Dec 27 17:15:40 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 28 16:58:27 2018 +0100
@@ -660,6 +660,8 @@
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
+    sessions_structure =>
+
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
 
@@ -737,13 +739,48 @@
       new Structure(restrict(build_graph), restrict(imports_graph))
     }
 
-    def selection_deps(sel: Selection,
+    def selection_deps(
+      options: Options,
+      selection: Selection,
       progress: Progress = No_Progress,
+      uniform_session: Boolean = false,
+      loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
       verbose: Boolean = false): Deps =
     {
-      Sessions.deps(selection(sel), global_theories,
-        progress = progress, inlined_files = inlined_files, verbose = verbose)
+      val selection1 =
+        if (uniform_session) {
+          val sessions_structure1 = sessions_structure.selection(selection)
+
+          val default_record_proofs = options.int("record_proofs")
+          val sessions_record_proofs =
+            for {
+              name <- sessions_structure1.build_topological_order
+              info <- sessions_structure1.get(name)
+              if info.options.int("record_proofs") > default_record_proofs
+            } yield name
+
+          val excluded =
+            for (name <- sessions_structure1.build_descendants(sessions_record_proofs))
+            yield {
+              progress.echo_warning("Skipping session " + name + "  (option record_proofs)")
+              name
+            }
+
+          selection.copy(exclude_sessions = excluded ::: selection.exclude_sessions)
+        }
+        else selection
+
+      val deps =
+        Sessions.deps(sessions_structure.selection(selection1), global_theories,
+          progress = progress, inlined_files = inlined_files, verbose = verbose)
+
+      if (loading_sessions) {
+        val selection_size = deps.sessions_structure.build_graph.size
+        if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
+      }
+
+      deps
     }
 
     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
diff -r 9403ff523825 -r fa94f2b2a877 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Dec 27 17:15:40 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Fri Dec 28 16:58:27 2018 +0100
@@ -88,7 +88,7 @@
 
     val deps =
       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
-        selection_deps(selection)
+        selection_deps(dump_options, selection, uniform_session = true, loading_sessions = true)
 
     val include_sessions =
       deps.sessions_structure.imports_topological_order
diff -r 9403ff523825 -r fa94f2b2a877 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Thu Dec 27 17:15:40 2018 +0100
+++ b/src/Pure/Tools/imports.scala	Fri Dec 28 16:58:27 2018 +0100
@@ -101,7 +101,7 @@
   {
     val deps =
       Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
-        selection_deps(selection, progress = progress, verbose = verbose).check_errors
+        selection_deps(options, selection, progress = progress, verbose = verbose).check_errors
 
     val root_keywords = Sessions.root_syntax.keywords