theory StoringData

imports "../Base"

begin

section {* Storing Data (TBD)\label{rec:storingdata} *} 

text {*

  {\bf Problem:} 

  Your tool needs to manage data.\smallskip

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

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

  context.

  *}

ML{*local

structure Data = GenericDataFun

 ( type T = int Symtab.table

   val empty = Symtab.empty

   val extend = I

   fun merge _ = Symtab.merge (K true)

 )

in

 val lookup = Symtab.lookup o Data.get

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

end *}

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

text {*

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

*}

text {*

  alternatives: TheoryDataFun, ProofDataFun

  Code: Pure/context.ML *}

end