# 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