theory Base

imports Main LaTeXsugar

uses

  "output_tutorial.ML"

  "antiquote_setup.ML"

begin

(* rebinding of writeln and tracing so that it can *)

(* be compared in intiquotations                   *)

ML {* 

fun writeln s = (Output.writeln s; s)

fun tracing s = (Output.tracing s; s)

*}

(* re-definition of various ML antiquotations    *)

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

ML {*

(* FIXME ref *)

fun write_file txt =

  case !file_name of

    NONE => () (* error "No open file" *)

  | SOME name => 

      (let 

         val stream = TextIO.openAppend name

       in

         TextIO.output (stream, txt); 

         TextIO.flushOut stream;                (* needed ?*)

         TextIO.closeOut stream

       end)

*}

ML {*

fun write_file_blk txt =

let

  val pre  = implode ["\n", "ML ", "{", "*", "\n"]

  val post = implode ["\n", "*", "}", "\n"]

in

  write_file (enclose pre post txt)

end

*}

ML {*

fun open_file name =

  (tracing ("Opened File: " ^ name);

   file_name := SOME name;

   TextIO.openOut name; ())

fun open_file_prelude name txt =

  (open_file name; write_file (txt ^ "\n"))

*}

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.position OuterParse.text >> (fn (txt, pos) =>

      Toplevel.generic_theory

        (ML_Context.exec (fn () => (write_file_blk txt; 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