--- a/ProgTutorial/Base.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Base.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,8 +1,8 @@
 theory Base
 imports Main LaTeXsugar
 uses
-  "output_tutorial.ML"
-  "antiquote_setup.ML"
+  ("output_tutorial.ML")
+  ("antiquote_setup.ML")
 begin
 
 (* rebinding of writeln and tracing so that it can *)
@@ -12,61 +12,97 @@
 fun tracing s = (Output.tracing s; s)
 *}
 
-(* re-definition of various ML antiquotations    *)
-(* to have a special tag for text enclosed in ML *)
+(* re-definition of various ML antiquotations     *)
+(* to have a special tag for text enclosed in ML; *)
+(* they also write the code into a separate file  *)
 
 ML {*
-(* FIXME ref *)
-val file_name = Unsynchronized.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)
+val (filename, setup_filename) = Attrib.config_string "filename" "File_Code.ML"
 *}
 
+setup {* setup_filename *}
+
 ML {*
-fun write_file_blk txt =
-let
-  val pre  = implode ["\n", "ML ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
+fun write_file txt thy =
+let 
+  val stream = Config.get_thy thy filename
+               |> TextIO.openAppend 
 in
-  write_file (enclose pre post txt)
+  TextIO.output (stream, txt); 
+  TextIO.flushOut stream;       (* needed ?*)
+  TextIO.closeOut stream
 end
 *}
 
 ML {*
-fun open_file name =
-  (tracing ("Opened File: " ^ name);
-   file_name := SOME name;
-   TextIO.openOut name; ())
+fun write_file_ml_blk txt thy =
+let
+  val pre  = implode ["\n", "ML ", "{", "*", "\n"]
+  val post = implode ["\n", "*", "}", "\n"]
+  val _ = write_file (enclose pre post txt) thy
+in
+  thy
+end
 
-fun open_file_prelude name txt =
-  (open_file name; write_file (txt ^ "\n"))
+fun write_file_setup_blk txt thy =
+let
+  val pre  = implode ["\n", "setup ", "{", "*", "\n"]
+  val post = implode ["\n", "*", "}", "\n"]
+  val _ = write_file (enclose pre post txt) thy
+in
+  thy
+end
+
+fun write_file_lsetup_blk txt lthy =
+let
+  val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]
+  val post = implode ["\n", "*", "}", "\n"]
+  val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy)
+in
+  lthy
+end
+
 *}
 
 ML {*
+fun open_file name thy =
+let  
+  val _ = tracing ("Open File: " ^ name)
+  val _ = TextIO.openOut name
+in 
+  Config.put_thy filename name thy
+end
+*}
 
+ML {*
+fun open_file_with_prelude name txts thy =
+let 
+  val thy' = open_file name thy 
+  val _ = write_file (cat_lines txts) thy'
+in
+  thy'
+end
+*}
+
+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
+*}
 
+ML {*
 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)))
+    (OuterParse.position OuterParse.text >> 
+      (fn (txt, pos) =>
+        Toplevel.generic_theory
+         (ML_Context.exec 
+           (fn () => ML_Context.eval true pos txt) 
+              #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
 
 val _ =
   OuterSyntax.command "ML_prf" "ML text within proof" 
@@ -79,7 +115,31 @@
   OuterSyntax.command "ML_val" "diagnostic ML text" 
   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
     (OuterParse.ML_source >> IsarCmd.ml_diag true)
+*}
 
+ML {*
+val _ =
+  OuterSyntax.command "setup" "ML theory setup" 
+    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
+      (OuterParse.ML_source >> (fn (txt, pos) => 
+        (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
 *}
 
+ML {* Context.proof_map *}
+ML {* IsarCmd.local_setup ; Context.map_proof (write_file_lsetup_blk "") *}
+
+
+ML {*
+val _ =
+  OuterSyntax.local_theory "local_setup" "ML local theory setup" 
+    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
+      (OuterParse.ML_source >> (fn (txt, pos) => 
+         IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
+*}
+
+
+use "output_tutorial.ML"
+use "antiquote_setup.ML"
+
+
 end
\ No newline at end of file