src/Pure/Thy/thy_read.ML
changeset 426 767367131b47
parent 424 f9d7e4fe141a
child 476 836cad329311
equal deleted inserted replaced
425:c42f384c89de 426:767367131b47
   388                          else
   388                          else
   389                            t :: (add loaded)
   389                            t :: (add loaded)
   390                       end
   390                       end
   391                   | add [] =
   391                   | add [] =
   392                       [ThyInfo {name = base, path = "", children = [child], 
   392                       [ThyInfo {name = base, path = "", children = [child], 
   393                                 thy_info = None, ml_info = None, theory = None}]
   393                                thy_info = None, ml_info = None, theory = None}]
   394             in loaded_thys := add (!loaded_thys) end;       
   394             in loaded_thys := add (!loaded_thys) end;       
   395 
   395 
   396           (*Load a base theory if not already done
   396           (*Load a base theory if not already done
   397             and no cycle would be created *)
   397             and no cycle would be created *)
   398           fun load base =
   398           fun load base =
   399               let val thy_present = already_loaded base
   399               let val thy_present = already_loaded base
   400                                             (*test this before child is added *)
   400                                            (*test this before child is added *)
   401               in
   401               in
   402                 if child = base then
   402                 if child = base then
   403                     error ("Cyclic dependency of theories: " ^ child
   403                     error ("Cyclic dependency of theories: " ^ child
   404                            ^ "->" ^ child)
   404                            ^ "->" ^ child)
   405                 else 
   405                 else 
   426             let val ThyInfo {theory, ...} = the (get_thyinfo name)
   426             let val ThyInfo {theory, ...} = the (get_thyinfo name)
   427             in the theory end;
   427             in the theory end;
   428 
   428 
   429           val mergelist = (unlink_thy child;
   429           val mergelist = (unlink_thy child;
   430                            load_base bases);
   430                            load_base bases);
   431           val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
       
   432                                                (*we have to return something *)
       
   433      in writeln ("Loading theory " ^ (quote child));
   431      in writeln ("Loading theory " ^ (quote child));
   434         foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
   432         merge_thy_list mk_draft (map get_theory mergelist) end;
   435 
   433 
   436 (*Change theory object for an existent item of loaded_thys 
   434 (*Change theory object for an existent item of loaded_thys 
   437   or create a new item *)
   435   or create a new item *)
   438 fun store_theory thy_name thy =
   436 fun store_theory thy_name thy =
   439   let fun make_change (t :: loaded) =
   437   let fun make_change (t :: loaded) =