4 Handling of named and nested targets at the Isar toplevel via context begin / end blocks. |
4 Handling of named and nested targets at the Isar toplevel via context begin / end blocks. |
5 *) |
5 *) |
6 |
6 |
7 signature TARGET_CONTEXT = |
7 signature TARGET_CONTEXT = |
8 sig |
8 sig |
9 val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory |
9 val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T -> |
|
10 theory -> local_theory |
10 val end_named_cmd: local_theory -> Context.generic |
11 val end_named_cmd: local_theory -> Context.generic |
11 val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> |
12 val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> |
12 (local_theory -> Context.generic) * local_theory |
13 (local_theory -> Context.generic) * local_theory |
13 val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> |
14 val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> |
14 Context.generic -> local_theory |
15 Context.generic -> local_theory |
16 end; |
17 end; |
17 |
18 |
18 structure Target_Context: TARGET_CONTEXT = |
19 structure Target_Context: TARGET_CONTEXT = |
19 struct |
20 struct |
20 |
21 |
21 fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy |
22 fun prep_includes thy = |
22 | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy; |
23 map (Bundle.check (Proof_Context.init_global thy)); |
|
24 |
|
25 fun context_begin_named_cmd raw_includes ("-", _) thy = |
|
26 Named_Target.init (prep_includes thy raw_includes) "" thy |
|
27 | context_begin_named_cmd raw_includes name thy = |
|
28 Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy; |
23 |
29 |
24 val end_named_cmd = Context.Theory o Local_Theory.exit_global; |
30 val end_named_cmd = Context.Theory o Local_Theory.exit_global; |
25 |
31 |
26 fun switch_named_cmd NONE (Context.Theory thy) = |
32 fun switch_named_cmd NONE (Context.Theory thy) = |
27 (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy) |
33 (end_named_cmd, Named_Target.theory_init thy) |
28 | switch_named_cmd (SOME name) (Context.Theory thy) = |
34 | switch_named_cmd (SOME name) (Context.Theory thy) = |
29 (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy) |
35 (end_named_cmd, context_begin_named_cmd [] name thy) |
30 | switch_named_cmd NONE (Context.Proof lthy) = |
36 | switch_named_cmd NONE (Context.Proof lthy) = |
31 (Context.Proof o Local_Theory.reset, lthy) |
37 (Context.Proof o Local_Theory.reset, lthy) |
32 | switch_named_cmd (SOME name) (Context.Proof lthy) = |
38 | switch_named_cmd (SOME name) (Context.Proof lthy) = |
33 (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, |
39 (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, |
34 (context_begin_named_cmd name o Local_Theory.exit_global_nonbrittle) lthy); |
40 (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy); |
35 |
41 |
36 fun includes raw_incls lthy = |
42 fun includes raw_includes lthy = |
37 Bundle.includes (map (Bundle.check lthy) raw_incls) lthy; |
43 Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; |
38 |
44 |
39 fun context_begin_nested_cmd raw_incls raw_elems gthy = |
45 fun context_begin_nested_cmd raw_includes raw_elems gthy = |
40 gthy |
46 gthy |
41 |> Context.cases Named_Target.theory_init Local_Theory.assert |
47 |> Context.cases Named_Target.theory_init Local_Theory.assert |
42 |> includes raw_incls |
48 |> includes raw_includes |
43 |> Expression.read_declaration ([], []) I raw_elems |
49 |> Expression.read_declaration ([], []) I raw_elems |
44 |> (#4 o fst) |
50 |> (#4 o fst) |
45 |> Local_Theory.begin_nested |
51 |> Local_Theory.begin_nested |
46 |> snd; |
52 |> snd; |
47 |
53 |