8 sig |
8 sig |
9 type locale |
9 type locale |
10 |
10 |
11 val clear_idents: Proof.context -> Proof.context |
11 val clear_idents: Proof.context -> Proof.context |
12 val test_locale: theory -> string -> bool |
12 val test_locale: theory -> string -> bool |
13 val register_locale: string -> |
13 val register_locale: bstring -> |
14 (string * sort) list * (Binding.T * typ option * mixfix) list -> |
14 (string * sort) list * (Binding.T * typ option * mixfix) list -> |
15 term option * term list -> |
15 term option * term list -> |
16 (declaration * stamp) list * (declaration * stamp) list -> |
16 (declaration * stamp) list * (declaration * stamp) list -> |
17 ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list -> |
17 ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list -> |
18 ((string * Morphism.morphism) * stamp) list -> theory -> theory |
18 ((string * Morphism.morphism) * stamp) list -> theory -> theory |
102 structure LocalesData = TheoryDataFun |
102 structure LocalesData = TheoryDataFun |
103 ( |
103 ( |
104 type T = NameSpace.T * locale Symtab.table; |
104 type T = NameSpace.T * locale Symtab.table; |
105 (* locale namespace and locales of the theory *) |
105 (* locale namespace and locales of the theory *) |
106 |
106 |
107 val empty = (NameSpace.empty, Symtab.empty); |
107 val empty = NameSpace.empty_table; |
108 val copy = I; |
108 val copy = I; |
109 val extend = I; |
109 val extend = I; |
110 |
110 |
111 fun join_locales _ |
111 fun join_locales _ |
112 (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies}, |
112 (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies}, |
118 decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')), |
118 decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')), |
119 notes = s_merge (notes, notes'), |
119 notes = s_merge (notes, notes'), |
120 dependencies = s_merge (dependencies, dependencies') |
120 dependencies = s_merge (dependencies, dependencies') |
121 } |
121 } |
122 end; |
122 end; |
123 fun merge _ ((space1, locs1), (space2, locs2)) = |
123 fun merge _ = NameSpace.join_tables join_locales; |
124 (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2)); |
|
125 ); |
124 ); |
126 |
125 |
127 val intern = NameSpace.intern o #1 o LocalesData.get; |
126 val intern = NameSpace.intern o #1 o LocalesData.get; |
128 val extern = NameSpace.extern o #1 o LocalesData.get; |
127 val extern = NameSpace.extern o #1 o LocalesData.get; |
129 |
128 |
134 | NONE => error ("Unknown locale " ^ quote name); |
133 | NONE => error ("Unknown locale " ^ quote name); |
135 |
134 |
136 fun test_locale thy name = case get_locale thy name |
135 fun test_locale thy name = case get_locale thy name |
137 of SOME _ => true | NONE => false; |
136 of SOME _ => true | NONE => false; |
138 |
137 |
139 fun register_locale name parameters spec decls notes dependencies thy = |
138 fun register_locale bname parameters spec decls notes dependencies thy = |
140 thy |> LocalesData.map (fn (space, locs) => |
139 thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname, |
141 (NameSpace.declare_base (Sign.naming_of thy) name space, Symtab.update (name, |
140 Loc {parameters = parameters, spec = spec, decls = decls, notes = notes, |
142 Loc {parameters = parameters, spec = spec, decls = decls, notes = notes, |
141 dependencies = dependencies}) #> snd); |
143 dependencies = dependencies}) locs)); |
|
144 |
142 |
145 fun change_locale name f thy = |
143 fun change_locale name f thy = |
146 let |
144 let |
147 val Loc {parameters, spec, decls, notes, dependencies} = |
145 val Loc {parameters, spec, decls, notes, dependencies} = |
148 the_locale thy name; |
146 the_locale thy name; |