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