equal
deleted
inserted
replaced
8 sig |
8 sig |
9 exception UNDEF |
9 exception UNDEF |
10 type state |
10 type state |
11 val init_toplevel: unit -> state |
11 val init_toplevel: unit -> state |
12 val theory_toplevel: theory -> state |
12 val theory_toplevel: theory -> state |
13 val get_prev_theory: theory -> serial |
|
14 val is_toplevel: state -> bool |
13 val is_toplevel: state -> bool |
15 val is_theory: state -> bool |
14 val is_theory: state -> bool |
16 val is_proof: state -> bool |
15 val is_proof: state -> bool |
17 val is_skipped_proof: state -> bool |
16 val is_skipped_proof: state -> bool |
18 val level: state -> int |
17 val level: state -> int |
151 fun output_of (State (_, (_, output))) = output; |
150 fun output_of (State (_, (_, output))) = output; |
152 |
151 |
153 fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE)); |
152 fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE)); |
154 fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE)); |
153 fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE)); |
155 |
154 |
156 val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0); |
|
157 fun get_prev_theory thy = Config.get_global thy prev_theory; |
|
158 fun set_prev_theory (State (_, (SOME prev_thy, _))) (Theory gthy) = |
|
159 let |
|
160 val put = Config.put_global prev_theory (Context.theory_identifier prev_thy); |
|
161 val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put); |
|
162 in Theory gthy' end |
|
163 | set_prev_theory _ node = node; |
|
164 |
|
165 fun level state = |
155 fun level state = |
166 (case node_of state of |
156 (case node_of state of |
167 Toplevel => 0 |
157 Toplevel => 0 |
168 | Theory _ => 0 |
158 | Theory _ => 0 |
169 | Proof (prf, _) => Proof.level (Proof_Node.current prf) |
159 | Proof (prf, _) => Proof.level (Proof_Node.current prf) |
327 let |
317 let |
328 val prev_thy = previous_theory_of state; |
318 val prev_thy = previous_theory_of state; |
329 val state' = State (node_presentation node, (prev_thy, NONE)); |
319 val state' = State (node_presentation node, (prev_thy, NONE)); |
330 in apply_presentation (fn st => f int st) state' end) () |
320 in apply_presentation (fn st => f int st) state' end) () |
331 | (Transaction _, Toplevel) => raise UNDEF |
321 | (Transaction _, Toplevel) => raise UNDEF |
332 | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node) |
322 | (Transaction (f, g), node) => apply (fn x => f int x) g node |
333 | _ => raise UNDEF); |
323 | _ => raise UNDEF); |
334 |
324 |
335 fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
325 fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
336 | apply_union int (tr :: trs) state = |
326 | apply_union int (tr :: trs) state = |
337 apply_union int trs state |
327 apply_union int trs state |