theory Base

imports Main

uses

  "chunks.ML"

  "antiquote_setup.ML"

begin

(* to have a special tag for text enclosed in ML *)

ML {*

fun inherit_env (context as Context.Proof lthy) =

      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)

  | inherit_env context = context;

fun inherit_env_prf prf = Proof.map_contexts

  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf

val _ =

  OuterSyntax.command "ML" "eval ML text within theory"

    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)

    (OuterParse.ML_source >> (fn (txt, pos) =>

      Toplevel.generic_theory

        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));

val _ =

  OuterSyntax.command "ML_prf" "ML text within proof" 

    (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)

    (OuterParse.ML_source >> (fn (txt, pos) =>

      Toplevel.proof (Proof.map_context (Context.proof_map

        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))

val _ =

  OuterSyntax.command "ML_val" "diagnostic ML text" 

  (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    (OuterParse.ML_source >> IsarCmd.ml_diag true);

*}

end