1 theory Data_slot

     2 imports Main

     3 begin

     4 

     5 ML {*

     6   fun ML_exec prog = ML_Compiler.eval true Position.none

     7                         (ML_Lex.tokenize prog)

     8 

     9   fun prog_data_slot name tp empty  = 

    10   "structure " ^ name ^ " = Theory_Data ( " ^

    11   "type T = "^ tp ^" " ^

    12   "val empty = " ^ empty ^ " ; "^

    13   "val extend = I; "^

    14   "fun merge (x, y) = x) "^

    15   "fun "^ name ^ "_store v =  Context.>>(Context.map_theory (" ^ name ^".map (fn x => v))) "^

    16   "fun "^ name ^ "_get () = Context.>>>(Context.map_theory_result (fn th => "^

    17   "                                     ("^ name ^".get th, th))) "

    18 

    19   fun data_slot name tp empty  = ML_exec (prog_data_slot name tp empty)

    20   val empty_term = @{term "x"}

    21   val empty_cterm = @{cterm "x"}

    22   val empty_thm = @{thm ext}

    23 *}

    24 

    25 end