--- a/NEWS Tue Mar 25 10:37:10 2014 +0100
+++ b/NEWS Tue Mar 25 13:18:10 2014 +0100
@@ -38,6 +38,11 @@
"exception_trace", which may be also declared within the context via
"declare [[exception_trace = true]]". Minor INCOMPATIBILITY.
+* Command 'SML_file' reads and evaluates the given Standard ML file.
+Toplevel bindings are stored within the theory context; the initial
+environment is restricted to the Standard ML implementation of
+Poly/ML, without the add-ons of Isabelle/ML.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/etc/isar-keywords-ZF.el Tue Mar 25 10:37:10 2014 +0100
+++ b/etc/isar-keywords-ZF.el Tue Mar 25 13:18:10 2014 +0100
@@ -20,6 +20,7 @@
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
+ "SML_file"
"abbreviation"
"also"
"apply"
@@ -344,6 +345,7 @@
(defconst isar-keywords-theory-decl
'("ML"
"ML_file"
+ "SML_file"
"abbreviation"
"attribute_setup"
"axiomatization"
--- a/etc/isar-keywords.el Tue Mar 25 10:37:10 2014 +0100
+++ b/etc/isar-keywords.el Tue Mar 25 13:18:10 2014 +0100
@@ -20,6 +20,7 @@
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
+ "SML_file"
"abbreviation"
"adhoc_overloading"
"also"
@@ -482,6 +483,7 @@
(defconst isar-keywords-theory-decl
'("ML"
"ML_file"
+ "SML_file"
"abbreviation"
"adhoc_overloading"
"atom_decl"
--- a/src/Doc/IsarRef/Spec.thy Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Tue Mar 25 13:18:10 2014 +0100
@@ -1000,6 +1000,7 @@
text {*
\begin{matharray}{rcl}
+ @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
@@ -1011,7 +1012,7 @@
\end{matharray}
@{rail \<open>
- @@{command ML_file} @{syntax name}
+ (@@{command SML_file} | @@{command ML_file}) @{syntax name}
;
(@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
@@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
@@ -1021,6 +1022,14 @@
\begin{description}
+ \item @{command "SML_file"}~@{text "name"} reads and evaluates the
+ given Standard ML file. Top-level SML bindings are stored within
+ the theory context; the initial environment is restricted to the
+ Standard ML implementation of Poly/ML, without the many add-ons of
+ Isabelle/ML. Multiple @{command "SML_file"} commands may be used to
+ build larger Standard ML projects, independently of the regular
+ Isabelle/ML environment.
+
\item @{command "ML_file"}~@{text "name"} reads and evaluates the
given ML file. The current theory context is passed down to the ML
toplevel and may be modified, using @{ML "Context.>>"} or derived ML
--- a/src/Doc/antiquote_setup.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Mar 25 13:18:10 2014 +0100
@@ -99,7 +99,9 @@
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
- val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2));
+ val _ =
+ ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
+ (ml (toks1, toks2));
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Mar 25 10:37:10 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Mar 25 13:18:10 2014 +0100
@@ -120,7 +120,7 @@
ML_Lex.read Position.none "fn _ => (" @
ML_Lex.read_source source @
ML_Lex.read Position.none ");";
- val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
+ val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
in "" end);
*}
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 25 13:18:10 2014 +0100
@@ -145,7 +145,8 @@
\ val " ^ name ^
" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
\end;\n");
- in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
+ val flags = {SML = false, verbose = false};
+ in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
(* old-style defs *)
@@ -238,7 +239,7 @@
let val opt_ctxt =
try Toplevel.generic_theory_of state
|> Option.map (Context.proof_of #> Diag_State.put state)
- in ML_Context.eval_source_in opt_ctxt verbose source end);
+ in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
val diag_state = Diag_State.get;
--- a/src/Pure/Isar/isar_syn.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Mar 25 13:18:10 2014 +0100
@@ -268,17 +268,28 @@
(* use ML text *)
val _ =
+ Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
+ (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
+ let
+ val ([{lines, pos, ...}], thy') = files thy;
+ val source = {delimited = true, text = cat_lines lines, pos = pos};
+ in
+ thy' |> Context.theory_map
+ (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
+ end)));
+
+val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
+ (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
Local_Theory.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
(Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
+ (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
Proof.propagate_ml_env)));
val _ =
--- a/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 25 13:18:10 2014 +0100
@@ -54,4 +54,11 @@
allSig = fn _ => [],
allFunct = fn _ => []};
+val initial_val : (string * valueVal) list = [];
+val initial_type : (string * typeVal) list = [];
+val initial_fixity : (string * fixityVal) list = [];
+val initial_structure : (string * structureVal) list = [];
+val initial_signature : (string * signatureVal) list = [];
+val initial_functor : (string * functorVal) list = [];
+
end;
--- a/src/Pure/ML-Systems/polyml.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Tue Mar 25 13:18:10 2014 +0100
@@ -4,6 +4,24 @@
Compatibility wrapper for Poly/ML.
*)
+(* ML name space *)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+ val initial_val =
+ List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+ (#allVal global ());
+ val initial_type = #allType global ();
+ val initial_fixity = #allFix global ();
+ val initial_structure = #allStruct global ();
+ val initial_signature = #allSig global ();
+ val initial_functor = #allFunct global ();
+end;
+
+
(* ML system operations *)
use "ML-Systems/ml_system.ML";
@@ -94,13 +112,6 @@
(* ML compiler *)
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
use "ML-Systems/use_context.ML";
use "ML-Systems/compiler_polyml.ML";
--- a/src/Pure/ML/ml_compiler.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Mar 25 13:18:10 2014 +0100
@@ -11,7 +11,8 @@
val exn_message: exn -> string
val exn_error_message: exn -> unit
val exn_trace: (unit -> 'a) -> 'a
- val eval: bool -> Position.T -> ML_Lex.token list -> unit
+ type flags = {SML: bool, verbose: bool}
+ val eval: flags -> Position.T -> ML_Lex.token list -> unit
end
structure ML_Compiler: ML_COMPILER =
@@ -28,8 +29,11 @@
val exn_error_message = Output.error_message o exn_message;
fun exn_trace e = print_exception_trace exn_message e;
-fun eval verbose pos toks =
+type flags = {SML: bool, verbose: bool};
+
+fun eval {SML, verbose} pos toks =
let
+ val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
val line = the_default 1 (Position.line_of pos);
val file = the_default "ML" (Position.file_of pos);
val text = ML_Lex.flatten toks;
--- a/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 13:18:10 2014 +0100
@@ -74,10 +74,12 @@
(* eval ML source tokens *)
-fun eval verbose pos toks =
+type flags = {SML: bool, verbose: bool};
+
+fun eval {SML, verbose} pos toks =
let
val _ = Secure.secure_mltext ();
- val space = ML_Env.name_space;
+ val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
val opt_context = Context.thread_data ();
--- a/src/Pure/ML/ml_context.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Mar 25 13:18:10 2014 +0100
@@ -21,12 +21,12 @@
val trace: bool Config.T
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: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
- val eval_file: bool -> Path.T -> unit
- val eval_source: bool -> Symbol_Pos.source -> unit
- val eval_in: Proof.context option -> bool -> Position.T ->
+ 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 -> Symbol_Pos.source -> unit
+ val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
- val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
+ val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
Context.generic -> Context.generic
end
@@ -140,8 +140,10 @@
val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
val trace = Config.bool trace_raw;
-fun eval verbose pos ants =
+fun eval flags pos ants =
let
+ val non_verbose = {SML = #SML flags, verbose = false};
+
(*prepare source text*)
val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
val _ =
@@ -157,11 +159,11 @@
val _ =
Context.setmp_thread_data
(Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
- (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
+ (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
|> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
- val _ = ML_Compiler.eval verbose pos body;
- val _ = ML_Compiler.eval false Position.none reset_env;
+ val _ = ML_Compiler.eval flags pos body;
+ val _ = ML_Compiler.eval non_verbose Position.none reset_env;
in () end;
end;
@@ -169,29 +171,29 @@
(* derived versions *)
-fun eval_file verbose path =
+fun eval_file flags path =
let val pos = Path.position path
- in eval verbose pos (ML_Lex.read pos (File.read path)) end;
+ in eval flags pos (ML_Lex.read pos (File.read path)) end;
-fun eval_source verbose source =
- eval verbose (#pos source) (ML_Lex.read_source source);
+fun eval_source flags source =
+ eval flags (#pos source) (ML_Lex.read_source source);
-fun eval_in ctxt verbose pos ants =
+fun eval_in ctxt flags pos ants =
Context.setmp_thread_data (Option.map Context.Proof ctxt)
- (fn () => eval verbose pos ants) ();
+ (fn () => eval flags pos ants) ();
-fun eval_source_in ctxt verbose source =
+fun eval_source_in ctxt flags source =
Context.setmp_thread_data (Option.map Context.Proof ctxt)
- (fn () => eval_source verbose source) ();
+ (fn () => eval_source flags source) ();
fun expression pos bind body ants =
- exec (fn () => eval false pos
+ exec (fn () => eval {SML = false, verbose = false} pos
(ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
end;
fun use s =
- ML_Context.eval_file true (Path.explode s)
+ ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
handle ERROR msg => (writeln msg; error "ML error");
--- a/src/Pure/ML/ml_env.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 25 13:18:10 2014 +0100
@@ -1,12 +1,14 @@
(* Title: Pure/ML/ml_env.ML
Author: Makarius
-Local environment of ML results.
+Toplevel environment for Standard ML and Isabelle/ML within the
+implicit context.
*)
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
+ val SML_name_space: ML_Name_Space.T
val name_space: ML_Name_Space.T
val local_context: use_context
val check_functor: string -> unit
@@ -17,56 +19,112 @@
(* context data *)
+type tables =
+ ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table;
+
+fun merge_tables
+ ((val1, type1, fixity1, structure1, signature1, functor1),
+ (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2));
+
+type data = {bootstrap: bool, tables: tables, sml_tables: tables};
+
+fun make_data (bootstrap, tables, sml_tables) : data =
+ {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
+
structure Env = Generic_Data
(
- type T =
- bool * (*global bootstrap environment*)
- (ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table);
- val empty : T =
- (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
- fun extend (_, tabs) : T = (false, tabs);
- fun merge
- ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
- (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
- (false,
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2)));
+ type T = data
+ val empty =
+ make_data (true,
+ (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
+ (Symtab.make ML_Name_Space.initial_val,
+ Symtab.make ML_Name_Space.initial_type,
+ Symtab.make ML_Name_Space.initial_fixity,
+ Symtab.make ML_Name_Space.initial_structure,
+ Symtab.make ML_Name_Space.initial_signature,
+ Symtab.make ML_Name_Space.initial_functor));
+ fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
+ fun merge (data : T * T) =
+ make_data (false,
+ merge_tables (pairself #tables data),
+ merge_tables (pairself #sml_tables data));
);
val inherit = Env.put o Env.get;
-(* results *)
+(* SML name space *)
+
+val SML_name_space: ML_Name_Space.T =
+ let
+ fun lookup which name =
+ Context.the_thread_data ()
+ |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
+
+ fun all which () =
+ Context.the_thread_data ()
+ |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
+ |> sort_distinct (string_ord o pairself #1);
+
+ fun enter which entry =
+ Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
+ let val sml_tables' = which (Symtab.update entry) sml_tables
+ in make_data (bootstrap, tables, sml_tables') end));
+ in
+ {lookupVal = lookup #1,
+ lookupType = lookup #2,
+ lookupFix = lookup #3,
+ lookupStruct = lookup #4,
+ lookupSig = lookup #5,
+ lookupFunct = lookup #6,
+ enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
+ enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
+ enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
+ enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
+ enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
+ enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
+ allVal = all #1,
+ allType = all #2,
+ allFix = all #3,
+ allStruct = all #4,
+ allSig = all #5,
+ allFunct = all #6}
+ end;
+
+
+(* Isabelle/ML name space *)
val name_space: ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
|> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
|> append (sel2 ML_Name_Space.global ())
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
if is_some (Context.thread_data ()) then
- Context.>> (Env.map (fn (global, tabs) =>
+ Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
let
- val _ = if global then sel2 ML_Name_Space.global entry else ();
- val tabs' = ap1 (Symtab.update entry) tabs;
- in (global, tabs') end))
+ val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
+ val tables' = ap1 (Symtab.update entry) tables;
+ in make_data (bootstrap, tables', sml_tables) end))
else sel2 ML_Name_Space.global entry;
in
{lookupVal = lookup #1 #lookupVal,
--- a/src/Pure/ML/ml_thms.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML Tue Mar 25 13:18:10 2014 +0100
@@ -130,7 +130,7 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else
- ML_Compiler.eval true Position.none
+ ML_Compiler.eval {SML = false, verbose = true} Position.none
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
val _ = Theory.setup (Stored_Thms.put []);
in () end;
--- a/src/Pure/Pure.thy Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/Pure.thy Tue Mar 25 13:18:10 2014 +0100
@@ -14,7 +14,7 @@
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
and "theory" :: thy_begin % "theory"
- and "ML_file" :: thy_load % "ML"
+ and "SML_file" "ML_file" :: thy_load % "ML"
and "header" :: diag
and "chapter" :: thy_heading1
and "section" :: thy_heading2
--- a/src/Pure/Thy/thy_output.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 25 13:18:10 2014 +0100
@@ -639,7 +639,7 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
(fn {context, ...} => fn source =>
- (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
+ (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
Symbol_Pos.source_content source
|> #1
|> (if Config.get context quotes then quote else I)
--- a/src/Pure/pure_syn.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/pure_syn.ML Tue Mar 25 13:18:10 2014 +0100
@@ -25,7 +25,7 @@
val source = {delimited = true, text = cat_lines lines, pos = pos};
in
gthy
- |> ML_Context.exec (fn () => ML_Context.eval_source true source)
+ |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
|> Local_Theory.propagate_ml_env
|> Context.mapping provide (Local_Theory.background_theory provide)
end)));