more careful handling of auxiliary environment structure -- allow nested ML evaluation;

--- a/src/Pure/ML-Systems/ml_name_space.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -61,4 +61,6 @@
 val initial_signature : (string * signatureVal) list = [];
 val initial_functor : (string * functorVal) list = [];
 
+fun forget_global_structure (_: string) = ();
+
 end;

--- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -19,6 +19,7 @@
   val initial_structure = #allStruct global ();
   val initial_signature = #allSig global ();
   val initial_functor = #allFunct global ();
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
 end;
 
 
@@ -173,6 +174,7 @@
   use_text context (1, "pp") false
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
-val ml_make_string =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
+fun ml_make_string struct_name =
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
+    struct_name ^ ".ML_print_depth ())))))";
 

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -65,7 +65,7 @@
   val _ = default_print_depth 10;
 end;
 
-val ml_make_string = "(fn _ => \"?\")";
+fun ml_make_string (_: string) = "(fn _ => \"?\")";
 
 
 (*prompts*)

--- a/src/Pure/ML/ml_antiquotations.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -13,12 +13,14 @@
  (ML_Antiquotation.inline @{binding assert}
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
-  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+  ML_Antiquotation.inline @{binding make_string}
+    (Args.context >> (ml_make_string o ML_Context.struct_name)) #>
 
   ML_Antiquotation.declaration @{binding print}
     (Scan.lift (Scan.optional Args.name "Output.writeln"))
       (fn src => fn output => fn ctxt =>
         let
+          val struct_name = ML_Context.struct_name ctxt;
           val (_, pos) = Token.name_of_src src;
           val (a, ctxt') = ML_Context.variant "output" ctxt;
           val env =
@@ -26,7 +28,7 @@
             \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
             ML_Syntax.print_position pos ^ "));\n";
           val body =
-            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
+            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ml_make_string struct_name ^ " x); x))";
         in (K (env, body), ctxt') end));
 
 
@@ -52,7 +54,8 @@
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>
 
-  ML_Antiquotation.inline @{binding context} (Scan.succeed "Isabelle.ML_context") #>
+  ML_Antiquotation.inline @{binding context}
+    (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
 
   ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>

--- a/src/Pure/ML/ml_context.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -13,14 +13,13 @@
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
+  val struct_name: Proof.context -> string
   val variant: string -> Proof.context -> string * Proof.context
   type decl = Proof.context -> string * string
   val value_decl: string -> string -> Proof.context -> decl * Proof.context
   val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
-  val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
-    Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
   val eval_source: ML_Compiler.flags -> Input.source -> unit
@@ -52,20 +51,23 @@
 
 (** ML antiquotations **)
 
-(* unique names *)
+(* names for generated environment *)
 
 structure Names = Proof_Data
 (
-  type T = Name.context;
+  type T = string * Name.context;
   val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
-  fun init _ = init_names;
+  fun init _ = ("Isabelle0", init_names);
 );
 
+fun struct_name ctxt = #1 (Names.get ctxt);
+val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ());
+
 fun variant a ctxt =
   let
-    val names = Names.get ctxt;
+    val names = #2 (Names.get ctxt);
     val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
-    val ctxt' = Names.put names' ctxt;
+    val ctxt' = (Names.map o apsnd) (K names') ctxt;
   in (b, ctxt') end;
 
 
@@ -77,7 +79,7 @@
   let
     val (b, ctxt') = variant a ctxt;
     val env = "val " ^ b ^ " = " ^ s ^ ";\n";
-    val body = "Isabelle." ^ b;
+    val body = struct_name ctxt ^ "." ^ b;
     fun decl (_: Proof.context) = (env, body);
   in (decl, ctxt') end;
 
@@ -118,36 +120,32 @@
   Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
   >> uncurry Token.src;
 
-val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
-
-fun begin_env visible =
-  ML_Lex.tokenize
-    ("structure Isabelle =\nstruct\n\
+fun make_env name visible =
+  (ML_Lex.tokenize
+    ("structure " ^ name ^ " =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
      " (ML_Context.the_local_context ());\n\
      \val ML_print_depth =\n\
      \  let val default = ML_Options.get_print_depth ()\n\
-     \  in fn () => ML_Options.get_print_depth_default default end;\n");
+     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
+   ML_Lex.tokenize "end;");
 
-val end_env = ML_Lex.tokenize "end;";
-val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
+fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
 
 fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok
   | expanding (Antiquote.Antiq _) = true;
 
-in
-
 fun eval_antiquotes (ants, pos) opt_context =
   let
     val visible =
       (case opt_context of
         SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
       | _ => true);
-    val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
+    val opt_ctxt = Option.map Context.proof_of opt_context;
 
     val ((ml_env, ml_body), opt_ctxt') =
       if forall (not o expanding) ants
-      then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
+      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
           fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
@@ -176,13 +174,16 @@
           val ctxt =
             (case opt_ctxt of
               NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
-            | SOME ctxt => Context.proof_of ctxt);
+            | SOME ctxt => struct_begin ctxt);
 
+          val (begin_env, end_env) = make_env (struct_name ctxt) visible;
           val (decls, ctxt') = fold_map expand ants ctxt;
           val (ml_env, ml_body) =
             decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat;
-        in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
-  in ((ml_env @ end_env, ml_body), opt_ctxt') end;
+        in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end;
+  in ((ml_env, ml_body), opt_ctxt') end;
+
+in
 
 fun eval flags pos ants =
   let
@@ -191,22 +192,33 @@
     (*prepare source text*)
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
     val _ =
-      (case Option.map Context.proof_of env_ctxt of
+      (case env_ctxt of
         SOME ctxt =>
           if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
           then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
       | NONE => ());
 
-    (*prepare static ML environment*)
+    (*prepare environment*)
     val _ =
       Context.setmp_thread_data
-        (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
+        (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
         (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
       |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
 
+    (*eval body*)
     val _ = ML_Compiler.eval flags pos body;
-    val _ = ML_Compiler.eval non_verbose Position.none reset_env;
+
+    (*clear environment*)
+    val _ =
+      (case (env_ctxt, is_some (Context.thread_data ())) of
+        (SOME ctxt, true) =>
+          let
+            val name = struct_name ctxt;
+            val _ = ML_Compiler.eval non_verbose Position.none (reset_env name);
+            val _ = Context.>> (ML_Env.forget_structure name);
+          in () end
+      | _ => ());
   in () end;
 
 end;

--- a/src/Pure/ML/ml_env.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -8,6 +8,7 @@
 signature ML_ENV =
 sig
   val inherit: Context.generic -> Context.generic -> Context.generic
+  val forget_structure: string -> Context.generic -> Context.generic
   val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val local_context: use_context
   val local_name_space: ML_Name_Space.T
@@ -63,6 +64,14 @@
 
 val inherit = Env.put o Env.get;
 
+fun forget_structure name =
+  Env.map (fn {bootstrap, tables, sml_tables} =>
+    let
+      val _ = if bootstrap then ML_Name_Space.forget_global_structure name else ();
+      val tables' =
+        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
+    in make_data (bootstrap, tables', sml_tables) end);
+
 
 (* name space *)
 

--- a/src/Pure/ML/ml_thms.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -58,7 +58,7 @@
     val (name, ctxt') = ML_Context.variant kind ctxt;
     val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
 
-    val ml_body = "Isabelle." ^ name;
+    val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
     fun decl final_ctxt =
       if initial then
         let

--- a/src/Tools/Code/code_runtime.ML	Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Dec 10 19:24:54 2014 +0100
@@ -359,7 +359,7 @@
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
     val (ml_code, consts_map) = Lazy.force acc_code;
     val ml_code = if is_first then ml_code else "";
-    val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const);
+    val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const);
   in (ml_code, body) end;
 
 in