src/Pure/context.ML
changeset 22603 76c30440c9af
parent 22599 d920d38f1f02
child 22827 7dc27b37f7f7
equal deleted inserted replaced
22602:a165d9ed08b8 22603:76c30440c9af
    33   val pprint_thy: theory -> pprint_args -> unit
    33   val pprint_thy: theory -> pprint_args -> unit
    34   val pretty_abbrev_thy: theory -> Pretty.T
    34   val pretty_abbrev_thy: theory -> Pretty.T
    35   val str_of_thy: theory -> string
    35   val str_of_thy: theory -> string
    36   val check_thy: theory -> theory
    36   val check_thy: theory -> theory
    37   val eq_thy: theory * theory -> bool
    37   val eq_thy: theory * theory -> bool
       
    38   val thy_ord: theory * theory -> order
    38   val subthy: theory * theory -> bool
    39   val subthy: theory * theory -> bool
    39   val joinable: theory * theory -> bool
    40   val joinable: theory * theory -> bool
    40   val merge: theory * theory -> theory                     (*exception TERM*)
    41   val merge: theory * theory -> theory                     (*exception TERM*)
    41   val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    42   val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    42   val self_ref: theory -> theory_ref
    43   val self_ref: theory -> theory_ref
   268 
   269 
   269 
   270 
   270 (* equality and inclusion *)
   271 (* equality and inclusion *)
   271 
   272 
   272 val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
   273 val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
       
   274 val thy_ord = int_ord o pairself (#1 o #id o identity_of);
   273 
   275 
   274 fun proper_subthy
   276 fun proper_subthy
   275     (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   277     (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   276   Inttab.defined ids i orelse Inttab.defined iids i;
   278   Inttab.defined ids i orelse Inttab.defined iids i;
   277 
   279 
   363     in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   365     in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   364 
   366 
   365 fun maximal_thys thys =
   367 fun maximal_thys thys =
   366   thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
   368   thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
   367 
   369 
   368 val creation_order = rev_order o int_ord o pairself (#1 o #id o identity_of);
       
   369 
       
   370 fun begin_thy pp name imports =
   370 fun begin_thy pp name imports =
   371   if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   371   if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   372   else
   372   else
   373     let
   373     let
   374       val parents =
   374       val parents =
   375         maximal_thys (distinct eq_thy (map check_thy imports));
   375         maximal_thys (distinct eq_thy (map check_thy imports));
   376       val ancestors = sort_distinct creation_order (parents @ maps ancestors_of parents);
   376       val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
   377       val Theory ({id, ids, iids, ...}, data, _, _) =
   377       val Theory ({id, ids, iids, ...}, data, _, _) =
   378         (case parents of
   378         (case parents of
   379           [] => error "No parent theories"
   379           [] => error "No parent theories"
   380         | [thy] => extend_thy thy
   380         | [thy] => extend_thy thy
   381         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   381         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));