--- 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 *}
--- 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
--- 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
--- 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 *}
--- 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
--- 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
--- 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} *}
--- 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) *}
--- 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
(*<*)
--- 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} *}
--- 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 {*
--- 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 *}
--- 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
--- 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 {*
--- 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} *}
--- 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
--- 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
--- 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} *}
--- 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} *}
--- 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} *}
--- 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
--- 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} *}
--- 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 {*
--- 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 *)
Binary file progtutorial.pdf has changed