theory StoringData
imports "../Base"
begin

section {* Storing Data\label{recipe:storingdata} *} 


text {*
  {\bf Problem:} 
  Your tool needs to keep complex 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) *}

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

text {*
  alternatives: TheoryDataFun, ProofDataFun
  Code: Pure/context.ML *}

end