# HG changeset patch
# User wenzelm
# Date 1527281277 -7200
# Node ID cbee43ff4cebf557d82e30772e15dc4a68d7cd12
# Parent  b5d0318757f0a2376058549695140d84afe97b46
added command 'ML_export';

diff -r b5d0318757f0 -r cbee43ff4ceb NEWS
--- a/NEWS	Fri May 25 22:47:36 2018 +0200
+++ b/NEWS	Fri May 25 22:47:57 2018 +0200
@@ -358,6 +358,11 @@
 * Operation Export.export emits theory exports (arbitrary blobs), which
 are stored persistently in the session build database.
 
+* Command 'ML_export' exports ML toplevel bindings to the global
+bootstrap environment of the ML process. This allows ML evaluation
+without a formal theory context, e.g. in command-line tools like
+"isabelle process".
+
 
 *** System ***
 
diff -r b5d0318757f0 -r cbee43ff4ceb src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri May 25 22:47:36 2018 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 25 22:47:57 2018 +0200
@@ -1058,6 +1058,7 @@
     @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
     @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
     @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
@@ -1081,8 +1082,9 @@
       @@{command ML_file_debug} |
       @@{command ML_file_no_debug}) @{syntax name} ';'?
     ;
-    (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
-      @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
+    (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |
+      @@{command ML_val} | @@{command ML_command} | @@{command setup} |
+      @@{command local_setup}) @{syntax text}
     ;
     @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
@@ -1103,10 +1105,16 @@
   \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
   the given file is compiled.
 
-  \<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given
-  \<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory
+  \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.
+  Top-level ML bindings are stored within the (global or local) theory
   context.
 
+  \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are
+  exported to the global bootstrap environment of the ML process --- it has
+  has a lasting effect that cannot be retracted. This allows ML evaluation
+  without a formal theory context, e.g. for command-line tools via @{tool
+  process} @{cite "isabelle-system"}.
+
   \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
   Top-level ML bindings are stored within the proof context in a purely
   sequential fashion, disregarding the nested proof structure. ML bindings
diff -r b5d0318757f0 -r cbee43ff4ceb src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Fri May 25 22:47:36 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Fri May 25 22:47:57 2018 +0200
@@ -13,6 +13,8 @@
   val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
   val init_bootstrap: Context.generic -> Context.generic
   val SML_environment: bool Config.T
+  val set_bootstrap: bool -> Context.generic -> Context.generic
+  val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
   val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val context: ML_Compiler0.context
@@ -130,6 +132,12 @@
             in (val2, type1, fixity1, structure2, signature2, functor1) end);
     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
 
+fun set_bootstrap bootstrap =
+  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
+    make_data (bootstrap, tables, sml_tables, breakpoints));
+
+val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
+
 fun add_name_space {SML} (space: ML_Name_Space.T) =
   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     let
diff -r b5d0318757f0 -r cbee43ff4ceb src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri May 25 22:47:36 2018 +0200
+++ b/src/Pure/Pure.thy	Fri May 25 22:47:57 2018 +0200
@@ -23,7 +23,7 @@
   and "external_file" "bibtex_file" :: thy_load
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
-  and "SML_import" "SML_export" :: thy_decl % "ML"
+  and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
   and "simproc_setup" :: thy_decl % "ML"
@@ -191,6 +191,18 @@
       end));
 
 val _ =
+  Outer_Syntax.command ("ML_export", \<^here>)
+    "ML text within theory or local theory, and export to bootstrap environment"
+    (Parse.ML_source >> (fn source =>
+      Toplevel.generic_theory (fn context =>
+        context
+        |> ML_Env.set_bootstrap true
+        |> ML_Context.exec (fn () =>
+            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
+        |> ML_Env.restore_bootstrap context
+        |> Local_Theory.propagate_ml_env)));
+
+val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
     (Parse.ML_source >> (fn source =>
       Toplevel.proof (Proof.map_context (Context.proof_map