theory Config
imports Base
begin

section {* Configuration Options *} 


text {*
  {\bf Problem:} 
  You would like to enhance your tool with options which can be changed later on
  by the user.\smallskip

  {\bf Solution:} This can be achieved using configuration values.\smallskip

  *}

ML {*
val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false
val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0
val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string"
*}

setup "setup_bvalue o setup_ivalue o setup_svalue"

declare [[bvalue = true, ivalue = 3]]

text {*
  Note that this works without introducing a new command to modify the 
  configuration options. *}

ML {*
Config.get @{context} bvalue
*}

ML {*
Config.get_thy @{theory} ivalue
*}

setup {* Config.put_thy svalue "foo" *}

ML {* 
Config.get @{context} svalue
*}

ML {*
let val ctxt = Config.map ivalue (fn i => i + 1) @{context}
in Config.get ctxt ivalue end
*}


text {*
  Code: Pure/Isar/attrib.ML, Pure/config.ML

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

end