# HG changeset patch # User wenzelm # Date 1677602533 -3600 # Node ID 0d5994eef9e6c154de75b4580b7096ddce77f684 # Parent 1b56b5471c7dbde4d95be6e6c7ea0ce0344ff84e clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure; diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/ML/ml_console.scala Tue Feb 28 17:42:13 2023 +0100 @@ -71,12 +71,14 @@ options, logic, dirs = dirs, include_sessions = include_sessions).check_errors } + val session_heaps = + if (raw_ml_system) Nil + else ML_Process.session_heaps(store, session_background, logic = logic) + // process loop val process = - ML_Process(store, options, session_background, - logic = logic, args = List("-i"), redirect = true, - modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), - raw_ml_system = raw_ml_system) + ML_Process(options, session_background, session_heaps, args = List("-i"), redirect = true, + modes = if (raw_ml_system) Nil else modes ::: List("ASCII")) POSIX_Interrupt.handler { process.interrupt() } { new TTY_Loop(process.stdin, process.stdout).join() diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/ML/ml_process.scala Tue Feb 28 17:42:13 2023 +0100 @@ -12,12 +12,22 @@ object ML_Process { + def session_heaps( + store: Sessions.Store, + session_background: Sessions.Background, + logic: String = "" + ): List[Path] = { + val logic_name = Isabelle_System.default_logic(logic) + + session_background.sessions_structure.selection(logic_name). + build_requirements(List(logic_name)). + map(store.the_heap) + } + def apply( - store: Sessions.Store, options: Options, session_background: Sessions.Background, - logic: String = "", - raw_ml_system: Boolean = false, + session_heaps: List[Path], use_prelude: List[String] = Nil, eval_main: String = "", args: List[String] = Nil, @@ -27,18 +37,8 @@ redirect: Boolean = false, cleanup: () => Unit = () => () ): Bash.Process = { - val logic_name = Isabelle_System.default_logic(logic) - - val heaps: List[String] = - if (raw_ml_system) Nil - else { - session_background.sessions_structure.selection(logic_name). - build_requirements(List(logic_name)). - map(a => File.platform_path(store.the_heap(a))) - } - val eval_init = - if (heaps.isEmpty) { + if (session_heaps.isEmpty) { List( """ fun chapter (_: string) = (); @@ -61,7 +61,9 @@ else { List( "(PolyML.SaveState.loadHierarchy " + - ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)") + ML_Syntax.print_list( + ML_Syntax.print_string_bytes)(session_heaps.map(File.platform_path)) + + "; PolyML.print_depth 0)") } val eval_modes = @@ -70,13 +72,13 @@ // options - val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") + val eval_options = if (session_heaps.isEmpty) Nil else List("Options.load_default ()") val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) // session resources - val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()") + val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()") val init_session = Isabelle_System.tmp_file("init_session") Isabelle_System.chmod("600", File.path(init_session)) File.write(init_session, new Resources(session_background).init_session_yxml) @@ -84,7 +86,7 @@ // process val eval_process = proper_string(eval_main).getOrElse( - if (heaps.isEmpty) { + if (session_heaps.isEmpty) { "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) } else "Isabelle_Process.init ()") @@ -169,9 +171,10 @@ val store = Sessions.store(options) val session_background = Sessions.background(options, logic, dirs = dirs).check_errors + val session_heaps = ML_Process.session_heaps(store, session_background, logic = logic) val result = - ML_Process(store, options, session_background, - logic = logic, args = eval_args, modes = modes).result( + ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes) + .result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_)) diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/PIDE/headless.scala Tue Feb 28 17:42:13 2023 +0100 @@ -619,10 +619,11 @@ ): Session = { val session_name = session_background.session_name val session = new Session(session_name, options, resources) + val session_heaps = ML_Process.session_heaps(store, session_background, logic = session_name) progress.echo("Starting session " + session_name + " ...") - Isabelle_Process.start(store, options, session, session_background, - logic = session_name, modes = print_mode).await_startup() + Isabelle_Process.start( + options, session, session_background, session_heaps, modes = print_mode).await_startup() session } diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/System/isabelle_process.scala Tue Feb 28 17:42:13 2023 +0100 @@ -13,12 +13,10 @@ object Isabelle_Process { def start( - store: Sessions.Store, options: Options, session: Session, session_background: Sessions.Background, - logic: String = "", - raw_ml_system: Boolean = false, + session_heaps: List[Path], use_prelude: List[String] = Nil, eval_main: String = "", modes: List[String] = Nil, @@ -32,8 +30,7 @@ options. string.update("system_channel_address", channel.address). string.update("system_channel_password", channel.password) - ML_Process(store, ml_options, session_background, - logic = logic, raw_ml_system = raw_ml_system, + ML_Process(ml_options, session_background, session_heaps, use_prelude = use_prelude, eval_main = eval_main, modes = modes, cwd = cwd, env = env) } diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Tue Feb 28 17:42:13 2023 +0100 @@ -43,6 +43,7 @@ progress: Progress, verbose: Boolean, session_background: Sessions.Background, + session_heaps: List[Path], store: Sessions.Store, do_store: Boolean, resources: Resources, @@ -62,15 +63,11 @@ private lazy val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { - val parent = info.parent.getOrElse("") - val env = Isabelle_System.settings( List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) - val is_pure = Sessions.is_pure(session_name) - - val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil + val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { @@ -268,11 +265,10 @@ val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) - val process = - Isabelle_Process.start(store, options, session, session_background, - logic = parent, raw_ml_system = is_pure, - use_prelude = use_prelude, eval_main = eval_main, - cwd = info.dir.file, env = env) + val process = { + Isabelle_Process.start(options, session, session_background, session_heaps, + use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) + } val build_errors = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Tue Feb 28 17:42:13 2023 +0100 @@ -586,6 +586,12 @@ store.init_session_info(_, session_name)) val session_background = build_deps.background(session_name) + val session_heaps = + session_background.info.parent match { + case None => Nil + case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic) + } + val resources = new Resources(session_background, log = log, command_timings = build_context(session_name).old_command_timings) @@ -595,9 +601,9 @@ val (numa_node, state1) = _state.numa_next(build_context.numa_nodes) val node_info = Build_Job.Node_Info(build_context.hostname, numa_node) val job = - new Build_Job.Build_Session(progress, verbose, session_background, store, do_store, - resources, build_context.session_setup, build_deps.sources_shasum(session_name), - input_heaps, node_info) + new Build_Job.Build_Session(progress, verbose, session_background, session_heaps, + store, do_store, resources, build_context.session_setup, + build_deps.sources_shasum(session_name), input_heaps, node_info) _state = state1.add_running(session_name, job) job } diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Tue Feb 28 17:42:13 2023 +0100 @@ -297,6 +297,8 @@ for ((session_background, session) <- try_session) { val store = Sessions.store(options) + val session_heaps = + ML_Process.session_heaps(store, session_background, logic = session_background.session_name) session_.change(_ => Some(session)) @@ -306,8 +308,8 @@ dynamic_output.init() try { - Isabelle_Process.start(store, options, session, session_background, - modes = modes, logic = session_background.session_name).await_startup() + Isabelle_Process.start( + options, session, session_background, session_heaps, modes = modes).await_startup() reply_ok( "Welcome to Isabelle/" + session_background.session_name + Isabelle_System.isabelle_heading()) diff -r 1b56b5471c7d -r 0d5994eef9e6 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Feb 28 17:16:50 2023 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Feb 28 17:42:13 2023 +0100 @@ -162,11 +162,12 @@ val session = PIDE.session val session_background = PIDE.resources.session_background val store = sessions_store(options = options) + val session_heaps = + ML_Process.session_heaps(store, session_background, logic = session_background.session_name) session.phase_changed += PIDE.plugin.session_phase_changed - Isabelle_Process.start(store, store.options, session, session_background, - logic = session_background.session_name, + Isabelle_Process.start(store.options, session, session_background, session_heaps, modes = (space_explode(',', store.options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)