--- a/CookBook/Recipes/Config.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-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