general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
theory StoringDataimports "../Base"beginsection {* Storing Data\label{recipe: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{*localstructure 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