src/Pure/context.ML
changeset 29001 b97a3f808133
parent 28617 c9c1c8b28a62
child 29069 c7ba485581ae
equal deleted inserted replaced
29000:5e03bc760355 29001:b97a3f808133
     1 (*  Title:      Pure/context.ML
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
       
     3     Author:     Markus Wenzel, TU Muenchen
     2     Author:     Markus Wenzel, TU Muenchen
     4 
     3 
     5 Generic theory contexts with unique identity, arbitrarily typed data,
     4 Generic theory contexts with unique identity, arbitrarily typed data,
     6 monotonic development graph and history support.  Generic proof
     5 monotonic development graph and history support.  Generic proof
     7 contexts with arbitrarily typed data.
     6 contexts with arbitrarily typed data.
   390         (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
   389         (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
   391     in thy'' end;
   390     in thy'' end;
   392 
   391 
   393 fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   392 fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   394   let
   393   let
   395     val {name, version, intermediates} = history_of thy;
   394     val {name, ...} = history_of thy;
   396     val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
   395     val Theory (identity', data', ancestry', _) = name_thy name thy;
   397     val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
       
   398     val identity' = make_identity self id ids Inttab.empty;
       
   399     val history' = make_history name 0 [];
   396     val history' = make_history name 0 [];
   400     val thy'' = vitalize (Theory (identity', data', ancestry', history'));
   397     val thy' = vitalize (Theory (identity', data', ancestry', history'));
   401     val _ = List.app (fn r => r := thy'') rs;
   398   in thy' end);
   402   in thy'' end);
       
   403 
   399 
   404 
   400 
   405 (* theory data *)
   401 (* theory data *)
   406 
   402 
   407 structure TheoryData =
   403 structure TheoryData =