theory Base

imports Main LaTeXsugar

uses

  "output_tutorial.ML"

  "chunks.ML"

  "antiquote_setup.ML"

begin

(* re-definition of various ML antiquotations    *)

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

ML {*

fun propagate_env (context as Context.Proof lthy) =

      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)

  | propagate_env context = context

fun propagate_env_prf prf = Proof.map_contexts

  (Context.proof_map (ML_Env.inherit (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) #> propagate_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))) #> propagate_env_prf)))

val _ =

  OuterSyntax.command "ML_val" "diagnostic ML text" 

  (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    (OuterParse.ML_source >> IsarCmd.ml_diag true)

*}

end