1 theory Config

     2 imports Base

     3 begin

     4 

     5 section {* Configuration Options *} 

     6 

     7 

     8 text {*

     9   {\bf Problem:} 

    10   You would like to enhance your tool with options which can be changed later on

    11   by the user.\smallskip

    12 

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

    14 

    15   *}

    16 

    17 ML {*

    18 val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false

    19 val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0

    20 val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string"

    21 *}

    22 

    23 setup "setup_bvalue o setup_ivalue o setup_svalue"

    24 

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

    26 

    27 text {*

    28   Note that this works without introducing a new command to modify the 

    29   configuration options. *}

    30 

    31 ML {*

    32 Config.get @{context} bvalue

    33 *}

    34 

    35 ML {*

    36 Config.get_thy @{theory} ivalue

    37 *}

    38 

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

    40 

    41 ML {* 

    42 Config.get @{context} svalue

    43 *}

    44 

    45 ML {*

    46 let val ctxt = Config.map ivalue (fn i => i + 1) @{context}

    47 in Config.get ctxt ivalue end

    48 *}

    49 

    50 

    51 text {*

    52   Code: Pure/Isar/attrib.ML, Pure/config.ML

    53 

    54   Note: Avoid to use references for this purpose!

    55   *}

    56 

    57 end