theory StoringData
imports "../Base"
begin

section {* Storing Data\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