theory StoringData

imports "../Base"

begin

section {* Storing Data *} 

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