ProgTutorial/Base.thy
author Christian Urban <urbanc@in.tum.de>
Sat, 30 May 2009 17:40:20 +0200
changeset 256 1fb8d62c88a0
parent 255 ef1da1abee46
child 260 5accec94b6df
permissions -rw-r--r--
added some first index-information

theory Base
imports Main
uses
  "output_tutorial.ML"
  "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