10 val subthy: theory * theory -> bool |
10 val subthy: theory * theory -> bool |
11 val assert_super: theory -> theory -> theory |
11 val assert_super: theory -> theory -> theory |
12 val parents_of: theory -> theory list |
12 val parents_of: theory -> theory list |
13 val ancestors_of: theory -> theory list |
13 val ancestors_of: theory -> theory list |
14 val nodes_of: theory -> theory list |
14 val nodes_of: theory -> theory list |
15 val check_thy: theory -> theory_ref |
|
16 val deref: theory_ref -> theory |
|
17 val merge: theory * theory -> theory |
15 val merge: theory * theory -> theory |
18 val merge_refs: theory_ref * theory_ref -> theory_ref |
|
19 val merge_list: theory list -> theory |
16 val merge_list: theory list -> theory |
20 val checkpoint: theory -> theory |
|
21 val copy: theory -> theory |
|
22 val requires: theory -> string -> string -> unit |
17 val requires: theory -> string -> string -> unit |
23 val get_markup: theory -> Markup.T |
18 val get_markup: theory -> Markup.T |
24 val axiom_space: theory -> Name_Space.T |
19 val axiom_space: theory -> Name_Space.T |
25 val axiom_table: theory -> term Symtab.table |
20 val axiom_table: theory -> term Symtab.table |
26 val axioms_of: theory -> (string * term) list |
21 val axioms_of: theory -> (string * term) list |
53 |
48 |
54 val parents_of = Context.parents_of; |
49 val parents_of = Context.parents_of; |
55 val ancestors_of = Context.ancestors_of; |
50 val ancestors_of = Context.ancestors_of; |
56 fun nodes_of thy = thy :: ancestors_of thy; |
51 fun nodes_of thy = thy :: ancestors_of thy; |
57 |
52 |
58 val check_thy = Context.check_thy; |
|
59 val deref = Context.deref; |
|
60 |
|
61 val merge = Context.merge; |
53 val merge = Context.merge; |
62 val merge_refs = Context.merge_refs; |
|
63 |
54 |
64 fun merge_list [] = raise THEORY ("Empty merge of theories", []) |
55 fun merge_list [] = raise THEORY ("Empty merge of theories", []) |
65 | merge_list (thy :: thys) = Library.foldl merge (thy, thys); |
56 | merge_list (thy :: thys) = Library.foldl merge (thy, thys); |
66 |
|
67 val checkpoint : theory -> theory = I; (* FIXME dummy *) |
|
68 val copy : theory -> theory = I; (* FIXME dummy *) |
|
69 |
57 |
70 fun requires thy name what = |
58 fun requires thy name what = |
71 if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then () |
59 if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then () |
72 else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); |
60 else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); |
73 |
61 |