src/Pure/Isar/code.ML
changeset 25501 845883bd3a6b
parent 25485 33840a854e63
child 25597 34860182b250
equal deleted inserted replaced
25500:7a284dc85326 25501:845883bd3a6b
   381     in (exec, ref data) end;
   381     in (exec, ref data) end;
   382 );
   382 );
   383 
   383 
   384 val _ = Context.add_setup CodeData.init;
   384 val _ = Context.add_setup CodeData.init;
   385 
   385 
   386 fun ch r f = let val x = f (! r) in (r := x; x) end;
       
   387 fun thy_data f thy = f ((snd o CodeData.get) thy);
   386 fun thy_data f thy = f ((snd o CodeData.get) thy);
   388 
   387 
   389 fun get_ensure_init kind data_ref =
   388 fun get_ensure_init kind data_ref =
   390   case Datatab.lookup (! data_ref) kind
   389   case Datatab.lookup (! data_ref) kind
   391    of SOME x => x
   390    of SOME x => x