1 theory Config

     2 imports "../Base"

     3 begin

     4 

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

     6 

     7 

     8 text {*

     9   {\bf Problem:} 

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

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

    12 

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

    14 

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

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

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

    18 *}

    19 

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

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

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

    23 

    24 text {* 

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

    26   be set up with

    27 *}

    28 

    29 setup {* setup_bval *} 

    30 setup {* setup_ival *}

    31 

    32 text {* or on the ML-level *}

    33 

    34 ML{*setup_sval @{theory} *}

    35 

    36 text {*

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

    38 *}

    39 

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

    41 

    42 text {*

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

    44   function @{ML Config.get}:

    45 

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

    47 

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

    49 

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

    51 

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

    53 

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

    55 *}

    56 

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

    58 

    59 text {* 

    60   Now the retrival of this value yields:

    61 

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

    63 

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

    65   @{ML ival} can be done by:

    66 

    67   @{ML_response [display,gray] 

    68 "let 

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

    70 in 

    71   Config.get ctxt ival

    72 end" "4"}

    73 

    74   \begin{readmore}

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

    76   \end{readmore}

    77 

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

    79   that it avoid global references, which cause many headaches with the

    80   multithreaded execution of Isabelle.

    81   

    82   *}

    83 end