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+
−