1 theory StoringData

     2 imports "../Base"

     3 begin

     4 

     5 section {* Storing Data *} 

     6 

     7 

     8 text {*

     9   {\bf Problem:} 

    10   Your tool needs to keep complex 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 {*

    20 local

    21 

    22 structure Data = GenericDataFun

    23 (

    24   type T = int Symtab.table

    25   val empty = Symtab.empty

    26   val extend = I

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

    28 )

    29 

    30 in

    31 

    32 val lookup = Symtab.lookup o Data.get

    33 

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

    35 

    36 end

    37 *}

    38 

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

    40 

    41 ML {* lookup (Context.Proof @{context}) "foo" *}

    42 

    43 text {*

    44   alternatives: TheoryDataFun, ProofDataFun

    45   Code: Pure/context.ML *}

    46 

    47 end