# HG changeset patch # User wenzelm # Date 1571047657 -7200 # Node ID 545229df2f823acf4b4ff21593fc28cf25272a60 # Parent 8a43ce639d85eefa21b8ae19871d32b6d38e4404 clarified signature: static Dump.Context vs. dynamic Dump.Session; diff -r 8a43ce639d85 -r 545229df2f82 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sun Oct 13 17:17:40 2019 +0200 +++ b/src/Pure/Tools/dump.scala Mon Oct 14 12:07:37 2019 +0200 @@ -73,7 +73,7 @@ error("Unknown aspect " + quote(name)) - /* session */ + /* context and session */ sealed case class Args( session: Headless.Session, @@ -83,72 +83,79 @@ def print_node: String = snapshot.node_name.toString } - object Session + object Context { def apply( options: Options, - logic: String, aspects: List[Aspect] = Nil, progress: Progress = No_Progress, - log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, - selection: Sessions.Selection = Sessions.Selection.empty): Session = + selection: Sessions.Selection = Sessions.Selection.empty): Context = { - new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection) + val session_options: Options = + { + val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options + val options1 = + options0 + + "completion_limit=0" + + "ML_statistics=false" + + "parallel_proofs=0" + + "editor_tracing_messages=0" + + "editor_presentation" + (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) + } + + val deps: Sessions.Deps = + Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs). + selection_deps(session_options, selection, progress = progress, + uniform_session = true, loading_sessions = true).check_errors + + new Context(options, progress, dirs, select_dirs, session_options, deps) } } - class Session private( - options: Options, - logic: String, - aspects: List[Aspect], - progress: Progress, - log: Logger, - dirs: List[Path], - select_dirs: List[Path], - selection: Sessions.Selection) + class Context private( + val options: Options, + val progress: Progress, + val dirs: List[Path], + val select_dirs: List[Path], + val session_options: Options, + val deps: Sessions.Deps) { - /* context */ - - Build.build_logic(options, logic, build_heap = true, progress = progress, - dirs = dirs ::: select_dirs, strict = true) + def session_dirs: List[Path] = dirs ::: select_dirs - val dump_options: Options = - { - val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options - val options1 = - options0 + - "completion_limit=0" + - "ML_statistics=false" + - "parallel_proofs=0" + - "editor_tracing_messages=0" + - "editor_presentation" - (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) - } + def session(logic: String, log: Logger = No_Logger): Session = + new Session(this, logic, log) + } - val deps: Sessions.Deps = - Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs). - selection_deps(dump_options, selection, progress = progress, - uniform_session = true, loading_sessions = true).check_errors + class Session private[Dump](context: Context, logic: String, log: Logger) + { + /* resources */ + + private val progress = context.progress + + Build.build_logic(context.options, logic, build_heap = true, progress = progress, + dirs = context.session_dirs, strict = true) val resources: Headless.Resources = - Headless.Resources.make(dump_options, logic, progress = progress, log = log, - session_dirs = dirs ::: select_dirs, - include_sessions = deps.sessions_structure.imports_topological_order) + Headless.Resources.make(context.session_options, logic, progress = progress, log = log, + session_dirs = context.session_dirs, + include_sessions = context.deps.sessions_structure.imports_topological_order) val used_theories: List[Document.Node.Name] = { for { - (name, _) <- deps.used_theories_condition(dump_options, progress = progress) + (name, _) <- + context.deps.used_theories_condition(context.session_options, progress = progress) if !resources.session_base.loaded_theory(name.theory) } yield name } - /* run */ + /* process */ - def run(process_theory: Args => Unit, unicode_symbols: Boolean = false) + def process(process_theory: Args => Unit, unicode_symbols: Boolean = false) { val session = resources.start_session(progress = progress) @@ -251,15 +258,15 @@ output_dir: Path = default_output_dir, selection: Sessions.Selection = Sessions.Selection.empty) { - val session = - Session(options, logic, aspects = aspects, progress = progress, log = log, dirs = dirs, + val context = + Context(options, aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, selection = selection) - session.run((args: Args) => + context.session(logic, log = log).process((args: Args) => { progress.echo("Processing theory " + args.print_node + " ...") val aspect_args = - Aspect_Args(session.dump_options, session.deps, progress, output_dir, + Aspect_Args(context.session_options, context.deps, progress, output_dir, args.snapshot, args.status) aspects.foreach(_.operation(aspect_args)) }) diff -r 8a43ce639d85 -r 545229df2f82 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Sun Oct 13 17:17:40 2019 +0200 +++ b/src/Pure/Tools/update.scala Mon Oct 14 12:07:37 2019 +0200 @@ -16,11 +16,11 @@ select_dirs: List[Path] = Nil, selection: Sessions.Selection = Sessions.Selection.empty) { - val session = - Dump.Session(options, logic, progress = progress, log = log, dirs = dirs, - select_dirs = select_dirs, selection = selection) + val context = + Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs, + selection = selection) - val path_cartouches = session.dump_options.bool("update_path_cartouches") + val path_cartouches = context.session_options.bool("update_path_cartouches") def update_xml(xml: XML.Body): XML.Body = xml flatMap { @@ -36,7 +36,7 @@ case t => List(t) } - session.run((args: Dump.Args) => + context.session(logic, log = log).process((args: Dump.Args) => { progress.echo("Processing theory " + args.print_node + " ...")