src/Pure/Pure.thy
changeset 68276 cbee43ff4ceb
parent 67777 2d3c1091527b
child 68482 cb84beb84ca9
     1.1 --- a/src/Pure/Pure.thy	Fri May 25 22:47:36 2018 +0200
     1.2 +++ b/src/Pure/Pure.thy	Fri May 25 22:47:57 2018 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    and "external_file" "bibtex_file" :: thy_load
     1.5    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     1.6    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
     1.7 -  and "SML_import" "SML_export" :: thy_decl % "ML"
     1.8 +  and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
     1.9    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    1.10    and "ML_val" "ML_command" :: diag % "ML"
    1.11    and "simproc_setup" :: thy_decl % "ML"
    1.12 @@ -191,6 +191,18 @@
    1.13        end));
    1.14  
    1.15  val _ =
    1.16 +  Outer_Syntax.command ("ML_export", \<^here>)
    1.17 +    "ML text within theory or local theory, and export to bootstrap environment"
    1.18 +    (Parse.ML_source >> (fn source =>
    1.19 +      Toplevel.generic_theory (fn context =>
    1.20 +        context
    1.21 +        |> ML_Env.set_bootstrap true
    1.22 +        |> ML_Context.exec (fn () =>
    1.23 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
    1.24 +        |> ML_Env.restore_bootstrap context
    1.25 +        |> Local_Theory.propagate_ml_env)));
    1.26 +
    1.27 +val _ =
    1.28    Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
    1.29      (Parse.ML_source >> (fn source =>
    1.30        Toplevel.proof (Proof.map_context (Context.proof_map