89 val pretty_locales: theory -> bool -> Pretty.T |
89 val pretty_locales: theory -> bool -> Pretty.T |
90 val pretty_locale: theory -> bool -> string -> Pretty.T |
90 val pretty_locale: theory -> bool -> string -> Pretty.T |
91 val pretty_registrations: Proof.context -> string -> Pretty.T |
91 val pretty_registrations: Proof.context -> string -> Pretty.T |
92 val pretty_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> Pretty.T |
92 val pretty_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> Pretty.T |
93 val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list |
93 val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list |
|
94 type locale_dependency = |
|
95 {source: string, target: string, prefix: (string * bool) list, morphism: morphism, |
|
96 pos: Position.T, serial: serial} |
|
97 val dest_dependencies: theory list -> theory -> locale_dependency list |
94 end; |
98 end; |
95 |
99 |
96 structure Locale: LOCALE = |
100 structure Locale: LOCALE = |
97 struct |
101 struct |
98 |
102 |
99 datatype ctxt = datatype Element.ctxt; |
103 datatype ctxt = datatype Element.ctxt; |
100 |
104 |
101 |
105 |
102 (*** Locales ***) |
106 (*** Locales ***) |
103 |
107 |
104 type dep = {name: string, morphisms: morphism * morphism, serial: serial}; |
108 type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial}; |
|
109 fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2; |
105 |
110 |
106 fun make_dep (name, morphisms) : dep = |
111 fun make_dep (name, morphisms) : dep = |
107 {name = name, morphisms = morphisms, serial = serial ()}; |
112 {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()}; |
108 |
113 |
109 (*table of mixin lists, per list mixins in reverse order of declaration; |
114 (*table of mixin lists, per list mixins in reverse order of declaration; |
110 lists indexed by registration/dependency serial, |
115 lists indexed by registration/dependency serial, |
111 entries for empty lists may be omitted*) |
116 entries for empty lists may be omitted*) |
112 type mixin = (morphism * bool) * serial; |
117 type mixin = (morphism * bool) * serial; |
166 dependencies = dependencies', mixins = mixins', ...}) = |
171 dependencies = dependencies', mixins = mixins', ...}) = |
167 mk_locale |
172 mk_locale |
168 ((parameters, spec, intros, axioms, hyp_spec), |
173 ((parameters, spec, intros, axioms, hyp_spec), |
169 ((merge (eq_snd op =) (syntax_decls, syntax_decls'), |
174 ((merge (eq_snd op =) (syntax_decls, syntax_decls'), |
170 merge (eq_snd op =) (notes, notes')), |
175 merge (eq_snd op =) (notes, notes')), |
171 (merge (op = o apply2 #serial) (dependencies, dependencies'), |
176 (merge eq_dep (dependencies, dependencies'), |
172 (merge_mixins (mixins, mixins'))))); |
177 (merge_mixins (mixins, mixins'))))); |
173 |
178 |
174 structure Locales = Theory_Data |
179 structure Locales = Theory_Data |
175 ( |
180 ( |
176 type T = locale Name_Space.table; |
181 type T = locale Name_Space.table; |
751 parents = map #name (dependencies_of thy name), |
756 parents = map #name (dependencies_of thy name), |
752 body = pretty_locale thy false name}; |
757 body = pretty_locale thy false name}; |
753 val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); |
758 val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); |
754 in map make_node names end; |
759 in map make_node names end; |
755 |
760 |
|
761 type locale_dependency = |
|
762 {source: string, target: string, prefix: (string * bool) list, morphism: morphism, |
|
763 pos: Position.T, serial: serial}; |
|
764 |
|
765 fun dest_dependencies prev_thys thy = |
|
766 let |
|
767 fun remove_prev loc prev_thy deps = |
|
768 (case get_locale prev_thy loc of |
|
769 NONE => deps |
|
770 | SOME (Loc {dependencies = prev_deps, ...}) => |
|
771 if eq_list eq_dep (prev_deps, deps) then [] |
|
772 else subtract eq_dep prev_deps deps); |
|
773 fun result loc (dep: dep) = |
|
774 let val morphism = op $> (#morphisms dep) in |
|
775 {source = #name dep, |
|
776 target = loc, |
|
777 prefix = Morphism.binding_prefix morphism, |
|
778 morphism = morphism, |
|
779 pos = #pos dep, |
|
780 serial = #serial dep} |
|
781 end; |
|
782 fun add (loc, Loc {dependencies = deps, ...}) = |
|
783 fold (cons o result loc) (fold (remove_prev loc) prev_thys deps); |
|
784 in |
|
785 Name_Space.fold_table add (Locales.get thy) [] |
|
786 |> sort (int_ord o apply2 #serial) |
|
787 end; |
|
788 |
756 end; |
789 end; |