--- a/ProgTutorial/Base.thy Sun Aug 16 22:14:36 2009 +0200
+++ b/ProgTutorial/Base.thy Mon Aug 17 20:57:32 2009 +0200
@@ -10,6 +10,43 @@
(* 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;
+ 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)
+
+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)
@@ -17,21 +54,27 @@
fun propagate_env_prf prf = Proof.map_contexts
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
+*}
+ML {*
val _ =
OuterSyntax.command "ML" "eval ML text within theory"
(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
- (OuterParse.ML_source >> (fn (txt, pos) =>
+ (OuterParse.position OuterParse.text >> (fn (txt, pos) =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)))
+ (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env)))
+*}
+ML {*
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)))
+*}
+ML {*
val _ =
OuterSyntax.command "ML_val" "diagnostic ML text"
(OuterKeyword.tag "TutorialML" OuterKeyword.diag)