--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/Config.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,83 @@
+theory Config
+imports "../Base"
+begin
+
+section {* Configuration Options\label{rec:config} *} 
+
+
+text {*
+  {\bf Problem:} 
+  You would like to enhance your tool with options that can be changed 
+  by the user without having to resort to the ML-level.\smallskip
+
+  {\bf Solution:} This can be achieved using configuration values.\smallskip
+
+  Assume you want to control three values, say @{text bval} containing a
+  boolean,  @{text ival} containing an integer and @{text sval} 
+  containing a string. These values can be declared on the ML-level by
+*}
+
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+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
+*}
+
+setup {* setup_bval *} 
+setup {* setup_ival *}
+
+text {* or on the ML-level *}
+
+ML{*setup_sval @{theory} *}
+
+text {*
+  The user can now manipulate the values from within Isabelle with the command
+*}
+
+declare [[bval = true, ival = 3]]
+
+text {*
+  On the ML-level these values can be retrieved using the 
+  function @{ML Config.get}:
+
+  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+
+  @{ML_response [display,gray] "Config.get @{context} ival" "3"}
+
+  The function @{ML Config.put} manipulates the values. For example
+
+  @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
+
+  The same can be achieved using the command \isacommand{setup}.
+*}
+
+setup {* Config.put_thy sval "bar" *}
+
+text {* 
+  Now the retrival of this value yields:
+
+  @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
+
+  We can apply a function to a value using @{ML Config.map}. For example incrementing
+  @{ML ival} can be done by:
+
+  @{ML_response [display,gray] 
+"let 
+  val ctxt = Config.map ival (fn i => i + 1) @{context}
+in 
+  Config.get ctxt ival
+end" "4"}
+
+  \begin{readmore}
+  For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+  \end{readmore}
+
+  There are many good reasons to control parameters in this way. One is
+  that it avoid global references, which cause many headaches with the
+  multithreaded execution of Isabelle.
+  
+  *}
+end
\ No newline at end of file