63 val set_defsort: sort -> local_theory -> local_theory |
63 val set_defsort: sort -> local_theory -> local_theory |
64 val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory |
64 val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory |
65 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
65 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
66 val type_alias: binding -> string -> local_theory -> local_theory |
66 val type_alias: binding -> string -> local_theory -> local_theory |
67 val const_alias: binding -> string -> local_theory -> local_theory |
67 val const_alias: binding -> string -> local_theory -> local_theory |
68 val init: Name_Space.naming -> operations -> Proof.context -> local_theory |
68 val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} -> |
|
69 operations -> Proof.context -> local_theory |
|
70 val exit_of: local_theory -> local_theory -> Proof.context |
69 val exit: local_theory -> Proof.context |
71 val exit: local_theory -> Proof.context |
70 val exit_global: local_theory -> theory |
72 val exit_global: local_theory -> theory |
71 val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context |
73 val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context |
72 val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory |
74 val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory |
73 val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) -> |
75 val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory, |
|
76 exit: local_theory -> Proof.context} -> operations -> |
74 local_theory -> Binding.scope * local_theory |
77 local_theory -> Binding.scope * local_theory |
75 val open_target: local_theory -> Binding.scope * local_theory |
78 val open_target: local_theory -> Binding.scope * local_theory |
76 val close_target: local_theory -> local_theory |
79 val close_target: local_theory -> local_theory |
77 end; |
80 end; |
78 |
81 |
93 declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory, |
96 declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory, |
94 theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
97 theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
95 local_theory -> local_theory, |
98 local_theory -> local_theory, |
96 locale_dependency: string * morphism -> (morphism * bool) option -> morphism -> |
99 locale_dependency: string * morphism -> (morphism * bool) option -> morphism -> |
97 local_theory -> local_theory, |
100 local_theory -> local_theory, |
98 pretty: local_theory -> Pretty.T list, |
101 pretty: local_theory -> Pretty.T list}; |
99 exit: local_theory -> Proof.context}; |
|
100 |
102 |
101 type lthy = |
103 type lthy = |
102 {background_naming: Name_Space.naming, |
104 {background_naming: Name_Space.naming, |
103 operations: operations, |
105 operations: operations, |
104 after_close: local_theory -> local_theory, |
106 after_close: local_theory -> local_theory, |
|
107 exit: local_theory -> Proof.context, |
105 brittle: bool, |
108 brittle: bool, |
106 target: Proof.context}; |
109 target: Proof.context}; |
107 |
110 |
108 fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy = |
111 fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy = |
109 {background_naming = background_naming, operations = operations, |
112 {background_naming = background_naming, operations = operations, |
110 after_close = after_close, brittle = brittle, target = target}; |
113 after_close = after_close, exit = exit, brittle = brittle, target = target}; |
111 |
114 |
112 |
115 |
113 (* context data *) |
116 (* context data *) |
114 |
117 |
115 structure Data = Proof_Data |
118 structure Data = Proof_Data |
144 val bottom_of = List.last o Data.get o assert; |
147 val bottom_of = List.last o Data.get o assert; |
145 val top_of = hd o Data.get o assert; |
148 val top_of = hd o Data.get o assert; |
146 |
149 |
147 fun map_top f = |
150 fun map_top f = |
148 assert #> |
151 assert #> |
149 Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents => |
152 Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents => |
150 make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents); |
153 make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents); |
151 |
154 |
152 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); |
155 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); |
153 |
156 |
154 fun map_contexts f lthy = |
157 fun map_contexts f lthy = |
155 let val n = level lthy in |
158 let val n = level lthy in |
156 lthy |> (Data.map o map_index) |
159 lthy |> (Data.map o map_index) |
157 (fn (i, {background_naming, operations, after_close, brittle, target}) => |
160 (fn (i, {background_naming, operations, after_close, exit, brittle, target}) => |
158 make_lthy (background_naming, operations, after_close, brittle, |
161 make_lthy (background_naming, operations, after_close, exit, brittle, |
159 target |
162 target |
160 |> Context_Position.set_visible false |
163 |> Context_Position.set_visible false |
161 |> f (n - i - 1) |
164 |> f (n - i - 1) |
162 |> Context_Position.restore_visible target)) |
165 |> Context_Position.restore_visible target)) |
163 |> f n |
166 |> f n |
166 |
169 |
167 (* brittle context -- implicit for nested structures *) |
170 (* brittle context -- implicit for nested structures *) |
168 |
171 |
169 fun mark_brittle lthy = |
172 fun mark_brittle lthy = |
170 if level lthy = 1 then |
173 if level lthy = 1 then |
171 map_top (fn (background_naming, operations, after_close, _, target) => |
174 map_top (fn (background_naming, operations, after_close, exit, _, target) => |
172 (background_naming, operations, after_close, true, target)) lthy |
175 (background_naming, operations, after_close, exit, true, target)) lthy |
173 else lthy; |
176 else lthy; |
174 |
177 |
175 fun assert_nonbrittle lthy = |
178 fun assert_nonbrittle lthy = |
176 if #brittle (top_of lthy) then error "Brittle local theory context" |
179 if #brittle (top_of lthy) then error "Brittle local theory context" |
177 else lthy; |
180 else lthy; |
180 (* naming for background theory *) |
183 (* naming for background theory *) |
181 |
184 |
182 val background_naming_of = #background_naming o top_of; |
185 val background_naming_of = #background_naming o top_of; |
183 |
186 |
184 fun map_background_naming f = |
187 fun map_background_naming f = |
185 map_top (fn (background_naming, operations, after_close, brittle, target) => |
188 map_top (fn (background_naming, operations, after_close, exit, brittle, target) => |
186 (f background_naming, operations, after_close, brittle, target)); |
189 (f background_naming, operations, after_close, exit, brittle, target)); |
187 |
190 |
188 val restore_background_naming = map_background_naming o K o background_naming_of; |
191 val restore_background_naming = map_background_naming o K o background_naming_of; |
189 |
192 |
190 val full_name = Name_Space.full_name o background_naming_of; |
193 val full_name = Name_Space.full_name o background_naming_of; |
191 |
194 |
346 |
349 |
347 (** manage targets **) |
350 (** manage targets **) |
348 |
351 |
349 (* outermost target *) |
352 (* outermost target *) |
350 |
353 |
351 fun init background_naming operations target = |
354 fun init {background_naming, exit} operations target = |
352 target |> Data.map |
355 target |> Data.map |
353 (fn [] => [make_lthy (background_naming, operations, I, false, target)] |
356 (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)] |
354 | _ => error "Local theory already initialized"); |
357 | _ => error "Local theory already initialized"); |
355 |
358 |
356 val exit = operation #exit; |
359 val exit_of = #exit o top_of; |
|
360 |
|
361 fun exit lthy = exit_of lthy lthy; |
357 val exit_global = Proof_Context.theory_of o exit; |
362 val exit_global = Proof_Context.theory_of o exit; |
358 |
363 |
359 fun exit_result f (x, lthy) = |
364 fun exit_result f (x, lthy) = |
360 let |
365 let |
361 val ctxt = exit lthy; |
366 val ctxt = exit lthy; |
370 in (f phi x, thy) end; |
375 in (f phi x, thy) end; |
371 |
376 |
372 |
377 |
373 (* nested targets *) |
378 (* nested targets *) |
374 |
379 |
375 fun init_target background_naming operations after_close lthy = |
380 fun init_target {background_naming, after_close, exit} operations lthy = |
376 let |
381 let |
377 val _ = assert lthy; |
382 val _ = assert lthy; |
378 val after_close' = Proof_Context.restore_naming lthy #> after_close; |
383 val after_close' = Proof_Context.restore_naming lthy #> after_close; |
379 val (scope, target) = Proof_Context.new_scope lthy; |
384 val (scope, target) = Proof_Context.new_scope lthy; |
380 val lthy' = |
385 val lthy' = |
381 target |
386 target |
382 |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target))); |
387 |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit, true, target))); |
383 in (scope, lthy') end; |
388 in (scope, lthy') end; |
384 |
389 |
385 fun open_target lthy = |
390 fun open_target lthy = |
386 init_target (background_naming_of lthy) (operations_of lthy) I lthy; |
391 init_target {background_naming = background_naming_of lthy, after_close = I, |
|
392 exit = exit_of lthy} (operations_of lthy) lthy; |
387 |
393 |
388 fun close_target lthy = |
394 fun close_target lthy = |
389 let |
395 let |
390 val _ = assert_not_bottom lthy; |
396 val _ = assert_not_bottom lthy; |
391 val ({after_close, ...} :: rest) = Data.get lthy; |
397 val ({after_close, ...} :: rest) = Data.get lthy; |