equal
deleted
inserted
replaced
49 val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory |
49 val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory |
50 val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory |
50 val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory |
51 val add_finals: bool -> string list -> theory -> theory |
51 val add_finals: bool -> string list -> theory -> theory |
52 val add_finals_i: bool -> term list -> theory -> theory |
52 val add_finals_i: bool -> term list -> theory -> theory |
53 val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory |
53 val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory |
54 val dep_graph: theory -> unit Graph.T; |
|
55 end |
54 end |
56 |
55 |
57 structure Theory: THEORY = |
56 structure Theory: THEORY = |
58 struct |
57 struct |
59 |
58 |
328 |
327 |
329 fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles => |
328 fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles => |
330 NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))]) |
329 NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))]) |
331 handle Symtab.DUPS dups => err_dup_oras dups); |
330 handle Symtab.DUPS dups => err_dup_oras dups); |
332 |
331 |
333 |
|
334 |
|
335 (** graph of theory parents **) |
|
336 |
|
337 fun dep_graph thy = |
|
338 let |
|
339 fun add_thy thy gr = |
|
340 let |
|
341 val name = Context.theory_name thy; |
|
342 in if can (Graph.get_node gr) name then (name, gr) |
|
343 else |
|
344 gr |
|
345 |> Graph.new_node (name, ()) |
|
346 |> fold_map add_thy (parents_of thy) |
|
347 |-> (fn names => fold (fn name' => Graph.add_edge (name, name')) names) |
|
348 |> pair name |
|
349 end; |
|
350 in snd (add_thy thy Graph.empty) end; |
|
351 |
|
352 end; |
332 end; |
353 |
333 |
354 structure BasicTheory: BASIC_THEORY = Theory; |
334 structure BasicTheory: BASIC_THEORY = Theory; |
355 open BasicTheory; |
335 open BasicTheory; |