theory Configimports "../Base"beginsection {* 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, namely @{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 with*}ML{*val (bval, setup_bval) = Attrib.config_bool "bval" falseval (ival, setup_ival) = Attrib.config_int "ival" 0val (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 by *}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 achived using the command \isacommand{setup}.*}setup {* Config.put_thy sval "bar" *}text {* The retrival of this value yields now @{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 ivalend" "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