theory Config
imports "../Base"
begin

section {* Configuration Options *} 


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 @{ML_text bval} containing a
  boolean,  @{ML_text ival} containing an integer and @{ML_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 is given a default. To enable these values, they need to 
  be set up using 
*}

setup {* setup_bval *} 
setup {* setup_ival *}

text {* or on the ML-level *}

ML {*
setup_sval @{theory} 
*}

text {*
  The user can now manipulate the values with the command
*}

declare [[bval = true, ival = 3]]

text {*
  from within Isabelle. On the ML-level these values can be retrieved using the 
  function @{ML Config.get}:

  @{ML_response [display] "Config.get @{context} bval" "true"}

  @{ML_response [display] "Config.get @{context} ival" "3"}

  The function @{ML Config.put} manipulates the values. For example

  @{ML_response [display] "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] "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] 
"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}

*}


text {*

  Note: Avoid to use references for this purpose!
  *}

end