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+
−