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 *)
val file_name = ref (NONE : string option)

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