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