# HG changeset patch
# User wenzelm
# Date 1460057237 -7200
# Node ID f37878ebba65d6c852246b75a104bccabc9ae72a
# Parent  5024d0c48e029d00a51cf42d61ed66ba3e1a9b3c
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
handle bootstrap signatures as well;

diff -r 5024d0c48e02 -r f37878ebba65 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 07 21:27:17 2016 +0200
@@ -272,12 +272,4 @@
     if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
 \<close>
 
-text \<open>Nested ML evaluation:\<close>
-ML \<open>
-  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
-  ML \<open>val b = @{thm sym}\<close>;
-  val c = @{thm trans}
-  val thms = [a, b, c];
-\<close>
-
 end
diff -r 5024d0c48e02 -r f37878ebba65 src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/HOL/ex/ML.thy	Thu Apr 07 21:27:17 2016 +0200
@@ -56,6 +56,17 @@
   val t = Syntax.read_term @{context} (Syntax.implode_input s);
 \<close>
 
+
+section \<open>Recursive ML evaluation\<close>
+
+ML \<open>
+  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
+  ML \<open>val b = @{thm sym}\<close>;
+  val c = @{thm trans}
+  val thms = [a, b, c];
+\<close>
+
+
 section \<open>IDE support\<close>
 
 text \<open>
diff -r 5024d0c48e02 -r f37878ebba65 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -144,7 +144,10 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
+    val space =
+      (case (#SML flags orelse #exchange flags, ML_Recursive.get ()) of
+        (false, SOME space) => space
+      | _ => ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags});
     val opt_context = Context.get_generic_context ();
 
 
@@ -264,7 +267,7 @@
 
     val _ =
       (while not (List.null (! input_buffer)) do
-        PolyML.compiler (get, parameters) ())
+        ML_Recursive.recursive space (fn () => PolyML.compiler (get, parameters) ()))
       handle exn =>
         if Exn.is_interrupt exn then Exn.reraise exn
         else
diff -r 5024d0c48e02 -r f37878ebba65 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -120,7 +120,11 @@
                 fold (fn (x, y) =>
                   member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
                 (#allStruct ML_Name_Space.global ()) structure1;
-            in (val2, type1, fixity1, structure2, signature1, functor1) end);
+              val signature2 =
+                fold (fn (x, y) =>
+                  member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
+                (#allSig ML_Name_Space.global ()) signature1;
+            in (val2, type1, fixity1, structure2, signature2, functor1) end);
     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
 
 fun add_name_space {SML} (space: ML_Name_Space.T) =
diff -r 5024d0c48e02 -r f37878ebba65 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -63,7 +63,10 @@
   val bootstrap_values =
     ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
   val bootstrap_structures =
-    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data"];
+    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data",
+      "ML_Recursive"];
+  val bootstrap_signatures =
+    ["THREAD_DATA", "ML_RECURSIVE"];
 
 
   (* Standard ML environment *)
@@ -74,6 +77,7 @@
   val sml_fixity = #allFix global ();
   val sml_structure =
     List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
-  val sml_signature = #allSig global ();
+  val sml_signature =
+    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
   val sml_functor = #allFunct global ();
 end;
diff -r 5024d0c48e02 -r f37878ebba65 src/Pure/ML/ml_recursive.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_recursive.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Pure/ML/ml_recursive.ML
+    Author:     Makarius
+
+ML name space for recursive compiler invocation.
+*)
+
+signature ML_RECURSIVE =
+sig
+  val get: unit -> PolyML.NameSpace.nameSpace option
+  val recursive: PolyML.NameSpace.nameSpace -> (unit -> 'a) -> 'a
+end;
+
+structure ML_Recursive: ML_RECURSIVE =
+struct
+
+val var = Thread_Data.var () : PolyML.NameSpace.nameSpace Thread_Data.var;
+
+fun get () = Thread_Data.get var;
+fun recursive space e = Thread_Data.setmp var (SOME space) e ();
+
+end;
diff -r 5024d0c48e02 -r f37878ebba65 src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/Pure/ROOT0.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -1,3 +1,4 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
 ML_file "Concurrent/thread_data.ML";
+ML_file "ML/ml_recursive.ML"