src/Pure/Thy/thy_read.ML
changeset 424 f9d7e4fe141a
parent 412 216624270b80
child 426 767367131b47
equal deleted inserted replaced
423:a42892e72854 424:f9d7e4fe141a
    26 
    26 
    27   val use_thy        : string -> unit
    27   val use_thy        : string -> unit
    28   val update         : unit -> unit
    28   val update         : unit -> unit
    29   val time_use_thy   : string -> unit
    29   val time_use_thy   : string -> unit
    30   val unlink_thy     : string -> unit
    30   val unlink_thy     : string -> unit
    31   val base_on        : basetype list -> string -> Thm.theory
    31   val base_on        : basetype list -> string -> bool -> Thm.theory
    32   val store_theory   : string -> Thm.theory -> unit
    32   val store_theory   : string -> Thm.theory -> unit
    33 end;
    33 end;
    34 
    34 
    35 
    35 
    36 functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
    36 functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
   341      reload_changed (load_order ["Pure"] [])
   341      reload_changed (load_order ["Pure"] [])
   342   end;
   342   end;
   343 
   343 
   344 (*Merge theories to build a base for a new theory.
   344 (*Merge theories to build a base for a new theory.
   345   Base members are only loaded if they are missing. *)
   345   Base members are only loaded if they are missing. *)
   346 fun base_on bases child =
   346 fun base_on bases child mk_draft =
   347       let (*List all descendants of a theory list *)
   347       let (*List all descendants of a theory list *)
   348           fun list_descendants (t :: ts) =
   348           fun list_descendants (t :: ts) =
   349                 let val tinfo = get_thyinfo t
   349                 let val tinfo = get_thyinfo t
   350                 in if is_some tinfo then
   350                 in if is_some tinfo then
   351                      let val ThyInfo {children, ...} = the tinfo
   351                      let val ThyInfo {children, ...} = the tinfo