1 theory StoringData

     2 imports "../Base"

     3 begin

     4 

     5 section {* Storing Data\label{rec:storingdata} *} 

     6 

     7 

     8 text {*

     9   {\bf Problem:} 

    10   Your tool needs to manage data.\smallskip

    11 

    12   {\bf Solution:} This can be achieved using a generic data slot.\smallskip

    13 

    14   Every generic data slot may keep data of any kind which is stored in the

    15   context.

    16 

    17   *}

    18 

    19 ML{*local

    20 

    21 structure Data = GenericDataFun

    22  ( type T = int Symtab.table

    23    val empty = Symtab.empty

    24    val extend = I

    25    fun merge _ = Symtab.merge (K true)

    26  )

    27 

    28 in

    29  val lookup = Symtab.lookup o Data.get

    30  fun update k v = Data.map (Symtab.update (k, v))

    31 end *}

    32 

    33 setup {* Context.theory_map (update "foo" 1) *}

    34 

    35 text {*

    36  

    37   @{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} 

    38 

    39 

    40 *}

    41 

    42 text {*

    43   alternatives: TheoryDataFun, ProofDataFun

    44   Code: Pure/context.ML *}

    45 

    46 end