# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255467445 -7200
# Node ID 0fea8b7a14a1a8c2eb6a47bb43934d2a8220bc1e
# Parent  4c54ef4dc84d98517f1a3731d0f1f766210c3919
tuned the ML-output mechanism; tuned slightly the text

diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Appendix.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,8 +1,15 @@
 
 theory Appendix
-imports Main
+imports Base
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "Recipes_Code.thy"
+  ["theory Recipes", "imports Main", "begin"]
+*}
+(*>*)
 
 text {* \appendix *}
 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Base.thy
--- 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
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/FirstSteps.ML
--- a/ProgTutorial/FirstSteps.ML	Mon Oct 12 17:07:17 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(* *)
-
-open_file_prelude 
-"FirstSteps_Code.thy"
-(cat_lines ["theory FirstSteps", "imports Base", "begin"])
\ No newline at end of file
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,8 +1,15 @@
 theory FirstSteps
 imports Base
-uses "FirstSteps.ML"
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "FirstSteps_Code.thy"
+  ["theory FirstSteps", "imports Main", "begin"]
+*}
+(*>*)
+
 chapter {* First Steps *}
 
 text {*
@@ -179,7 +186,8 @@
   You can print out error messages with the function @{ML_ind  error}; for 
   example:
 
-@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
+  @{ML_response_fake [display,gray] 
+  "if 0=1 then true else (error \"foo\")" 
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
@@ -1218,13 +1226,14 @@
 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
 
 text {* 
-  where each value needs to be given a default. To enable these values, they need to 
-  be set up with
+  where each value needs to be given a default. To enable these values on the 
+  user-level, they need to be set up with
 *}
 
 setup %gray {* 
   setup_bval #> 
-  setup_ival 
+  setup_ival #>
+  setup_sval
 *}
 
 text {*
@@ -1236,15 +1245,36 @@
 
 text {*
   On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}.
+  function @{ML_ind get in Config} from a proof context
+
+  @{ML_response [display,gray] 
+  "Config.get @{context} bval" 
+  "true"}
+
+  or from a theory using the function @{ML_ind get_thy in Config}
+
+  @{ML_response [display,gray] 
+  "Config.get_thy @{theory} bval" 
+  "true"}
 
-  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+  It is also possible to manipulate the configuration values
+  from the ML-level with the function @{ML_ind put in Config}
+  or @{ML_ind put_thy in Config}. For example
+
+  @{ML_response [display,gray]
+  "let
+  val ctxt = @{context}
+  val ctxt' = Config.put sval \"foo\" ctxt
+in
+  (Config.get ctxt sval, Config.get ctxt' sval)
+end"
+  "(\"some string\", \"foo\")"}
 
   \begin{readmore}
   For more information about configuration values see 
-  @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+  the files @{ML_file "Pure/Isar/attrib.ML"} and 
+  @{ML_file "Pure/config.ML"}.
   \end{readmore}
- 
 *}
 
 section {* Summary *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/General.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -2,7 +2,16 @@
 imports Base FirstSteps
 begin
 
-chapter {* Let's Talk About the Good, the Bad and the Ugly *}
+(*<*)
+setup{*
+open_file_with_prelude 
+  "General_Code.thy"
+  ["theory General", "imports Base FirstSteps", "begin"]
+*}
+(*>*)
+
+
+chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *}
 
 text {*
   Isabelle is build around a few central ideas. One central idea is the
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -2,9 +2,16 @@
 imports Base
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "Intro_Code.thy"
+  ["theory Intro", "imports Main", "begin"]
+*}
+(*>*)
+
 chapter {* Introduction *}
 
-
 text {*
    \begin{flushright}
   {\em
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Code
-imports "../Base" "../FirstSteps" Ind_General_Scheme
+imports Ind_General_Scheme "../FirstSteps" 
 begin
 
 section {* The Gory Details\label{sec:code} *} 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Extensions
-imports "../Base" Simple_Inductive_Package
+imports Simple_Inductive_Package Ind_Intro
 begin
 
 section {* Extensions of the Package (TBD) *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_General_Scheme.thy
--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_General_Scheme 
-imports  "../Base" Simple_Inductive_Package
+imports  Ind_Intro Simple_Inductive_Package
 begin
 
 (*<*)
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Interface
-imports "../Base" Simple_Inductive_Package
+imports Ind_Intro Simple_Inductive_Package
 begin
 
 section {* Parsing and Typing the Specification\label{sec:interface} *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_Intro.thy
--- a/ProgTutorial/Package/Ind_Intro.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,7 +1,15 @@
 theory Ind_Intro
-imports Main 
+imports "../Base"
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "Ind_Package_Code.thy"
+  ["theory Ind_Package", "imports Main", "begin"]
+*}
+(*>*)
+
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Package/Ind_Prelims.thy
--- a/ProgTutorial/Package/Ind_Prelims.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Prelims
-imports Main "../Base" 
+imports Ind_Intro 
 begin
 
 section{* Preliminaries *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Parsing.ML
--- a/ProgTutorial/Parsing.ML	Mon Oct 12 17:07:17 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(* *)
-
-open_file_prelude 
-"Parsing_Code.thy"
-(cat_lines ["theory Parsing", 
-            "imports Base \"Package/Simple_Inductive_Package\"", 
-            "begin"])
\ No newline at end of file
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,8 +1,17 @@
 theory Parsing
 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
-uses "Parsing.ML"
 begin
 
+(*<*)
+setup {*
+open_file_with_prelude 
+"Parsing_Code.thy"
+["theory Parsing", 
+ "imports Base \"Package/Simple_Inductive_Package\"", 
+ "begin"]
+*}
+(*>*)
+
 chapter {* Parsing *}
 
 text {*
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/Antiquotes.thy
--- a/ProgTutorial/Recipes/Antiquotes.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,6 +1,6 @@
 
 theory Antiquotes
-imports "../Base"
+imports "../Appendix"
 begin
 
 section {* Useful Document Antiquotations\label{rec:docantiquotations} *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/ExternalSolver.thy
--- a/ProgTutorial/Recipes/ExternalSolver.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory ExternalSolver
-imports "../Base"
+imports "../Appendix"
 begin
 
 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/Oracle.thy
--- a/ProgTutorial/Recipes/Oracle.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Oracle
-imports "../Base"
+imports "../Appendix"
 uses ("external_solver.ML")
 begin
 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,6 +1,6 @@
 
 theory Sat
-imports Main "../FirstSteps"
+imports "../Appendix" "../FirstSteps" 
 begin
 
 section {* SAT Solvers\label{rec:sat} *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/TimeLimit.thy
--- a/ProgTutorial/Recipes/TimeLimit.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory TimeLimit
-imports "../Base"
+imports "../Appendix"
 begin
 
 section {* Restricting the Runtime of a Function\label{rec:timeout} *} 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/Timing.thy
--- a/ProgTutorial/Recipes/Timing.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/Timing.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,5 +1,5 @@
 theory Timing
-imports "../Base"
+imports "../Appendix"
 begin
 
 section {* Measuring Time\label{rec:timing} *} 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Recipes/USTypes.thy
--- a/ProgTutorial/Recipes/USTypes.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Recipes/USTypes.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,6 +1,6 @@
 
 theory USTypes
-imports Main
+imports "../Appendix"
 begin
 
 
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -2,6 +2,14 @@
 imports FirstSteps "Recipes/Timing"
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "Solutions_Code.thy"
+  ["theory Solutions", "imports FirstSteps", "begin"]
+*}
+(*>*)
+
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
 text {* \solution{fun:revsum} *}
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -2,6 +2,14 @@
 imports Base FirstSteps
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "Tactical_Code.thy"
+  ["theory Tactical", "imports Base FirstSteps", "begin"]
+*}
+(*>*)
+
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Oct 13 22:57:25 2009 +0200
@@ -81,11 +81,13 @@
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
+     write_file_ml_blk lhs (Context.theory_of_proof ctxt);
      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE lhs);
+     write_file_ml_blk lhs (Context.theory_of_proof ctxt);
      output ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
diff -r 4c54ef4dc84d -r 0fea8b7a14a1 progtutorial.pdf
Binary file progtutorial.pdf has changed