1 theory Config

     2 imports "../Base"

     3 begin

     4 

     5 section {* Configuration Options\label{rec:config} *} 

     6 

     7 text {*

     8   {\bf Problem:} 

     9   You would like to enhance your tool with options that can be changed 

    10   by the user without having to resort to the ML-level.\smallskip

    11 

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

    13 

    14   Assume you want to control three values, say @{text bval} containing a

    15   boolean,  @{text ival} containing an integer and @{text sval} 

    16   containing a string. These values can be declared on the ML-level by

    17 *}

    18 

    19 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false

    20 val (ival, setup_ival) = Attrib.config_int "ival" 0

    21 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}

    22 

    23 text {* 

    24   where each value needs to be given a default. To enable these values, they need to 

    25   be set up with

    26 *}

    27 

    28 setup {* setup_bval *} 

    29 setup {* setup_ival *}

    30 

    31 text {* or on the ML-level with *}

    32 

    33 ML{*setup_sval @{theory} *}

    34 

    35 text {*

    36   The user can now manipulate the values from within Isabelle with the command

    37 *}

    38 

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

    40 

    41 text {*

    42   On the ML-level these values can be retrieved using the 

    43   function @{ML Config.get}:

    44 

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

    46 

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

    48 

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

    50 

    51   @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}

    52 

    53   The same can be achieved using the command \isacommand{setup}.

    54 *}

    55 

    56 setup {* Config.put_thy sval "bar" *}

    57 

    58 text {* 

    59   Now the retrieval of this value yields:

    60 

    61   @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}

    62 

    63   We can apply a function to a value using @{ML Config.map}. For example incrementing

    64   @{ML ival} can be done by:

    65 

    66   @{ML_response [display,gray] 

    67 "let 

    68   val ctxt' = Config.map ival (fn i => i + 1) @{context}

    69 in 

    70   Config.get ctxt' ival

    71 end" "4"}

    72 

    73   \begin{readmore}

    74   For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.

    75   \end{readmore}

    76 

    77   There are many good reasons to control parameters in this way. One is

    78   that no global reference is needed, which would cause many headaches 

    79   with the multithreaded execution of Isabelle.

    80 *}

    81 

    82 end