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 with *}+ −
+ −
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 retrieval 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 no global reference is needed, which would cause many headaches + −
with the multithreaded execution of Isabelle.+ −
*}+ −
+ −
end+ −