122 fun full_name lthy = |
122 fun full_name lthy = |
123 let |
123 let |
124 val naming = Sign.naming_of (ProofContext.theory_of lthy) |
124 val naming = Sign.naming_of (ProofContext.theory_of lthy) |
125 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
125 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
126 |> NameSpace.qualified_names; |
126 |> NameSpace.qualified_names; |
127 in NameSpace.full naming end; |
127 in NameSpace.full naming end; |
128 |
128 |
129 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
129 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
130 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
130 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
131 |> Sign.qualified_names |
131 |> Sign.qualified_names |
132 |> f |
132 |> f |
174 val args' = args |> filter (fn (t, _) => t aconv Morphism.term phi t); |
174 val args' = args |> filter (fn (t, _) => t aconv Morphism.term phi t); |
175 in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end; |
175 in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end; |
176 |
176 |
177 fun notation mode args = term_syntax (generic_notation mode args); |
177 fun notation mode args = term_syntax (generic_notation mode args); |
178 |
178 |
179 fun abbrevs mode args = term_syntax (fn phi => |
179 |
180 let |
180 fun morph_abbrev phi ((c, mx), t) = ((Morphism.name phi c, mx), Morphism.term phi t); |
181 val (mxs, args') = args |> map_filter (fn ((c, mx), t) => |
181 |
182 if t aconv Morphism.term phi t |
182 fun abbrevs mode raw_args lthy = |
183 then SOME (mx, ((Morphism.name phi c, NoSyn), t)) |
183 let val args = map (morph_abbrev (target_morphism lthy)) raw_args in |
184 else NONE) |
184 lthy |> term_syntax (fn phi => |
185 |> split_list; |
185 let |
186 in |
186 val args' = map (morph_abbrev phi) args; |
187 Context.mapping_result (Sign.add_abbrevs mode args') (ProofContext.add_abbrevs mode args') |
187 val (abbrs, mxs) = (args ~~ args') |> map_filter (fn ((_, rhs), ((c', mx'), rhs')) => |
188 #-> (fn abbrs => generic_notation mode (map #1 abbrs ~~ mxs) phi) |
188 if rhs aconv rhs' then SOME (((c', NoSyn), rhs'), mx') else NONE) |
189 end); |
189 |> split_list; |
|
190 in |
|
191 Context.mapping_result (Sign.add_abbrevs mode abbrs) (ProofContext.add_abbrevs mode abbrs) |
|
192 #-> (fn res => generic_notation mode (map #1 res ~~ mxs) phi) |
|
193 end) |
|
194 end; |
190 |
195 |
191 |
196 |
192 (* init -- exit *) |
197 (* init -- exit *) |
193 |
198 |
194 fun init theory_prefix operations target = target |> Data.map |
199 fun init theory_prefix operations target = target |> Data.map |