--- a/src/Pure/Tools/ml_process.scala Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala Fri Apr 07 19:35:39 2017 +0200
@@ -24,6 +24,7 @@
cleanup: () => Unit = () => (),
channel: Option[System_Channel] = None,
sessions: Option[Sessions.T] = None,
+ session_base: Option[Sessions.Base] = None,
store: Sessions.Store = Sessions.store()): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
@@ -89,6 +90,21 @@
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
+ // session base
+ val eval_session_base =
+ session_base match {
+ case None => Nil
+ case Some(base) =>
+ val known_theories =
+ for ((theory, node_name) <- base.known_theories.toList)
+ yield (theory, node_name.node)
+ List("Resources.set_session_base {known_theories = " +
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(
+ ML_Syntax.print_string, ML_Syntax.print_string))(known_theories) + "}")
+ }
+
+ // process
val eval_process =
if (heaps.isEmpty)
List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
@@ -114,7 +130,7 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_process).
+ (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
map(eval => List("--eval", eval)).flatten ::: args
Bash.process(