diff -r ed797395fab6 -r 007922777ff1 ProgTutorial/Base.thy
--- 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)