--- a/src/Pure/Isar/bundle.ML Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Wed Apr 01 13:32:32 2015 +0200
@@ -20,9 +20,10 @@
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: string list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
- val context: string list -> Element.context_i list -> generic_theory -> local_theory
+ val context: string list -> Element.context_i list ->
+ generic_theory -> Binding.scope * local_theory
val context_cmd: (xstring * Position.T) list -> Element.context list ->
- generic_theory -> local_theory
+ generic_theory -> Binding.scope * local_theory
val print_bundles: Proof.context -> unit
end;
@@ -97,7 +98,7 @@
|> gen_includes get raw_incls
|> prep_decl ([], []) I raw_elems;
in
- lthy' |> Local_Theory.open_target
+ lthy' |> Local_Theory.init_target
(Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
end;
@@ -137,4 +138,3 @@
end |> Pretty.writeln_chunks;
end;
-
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 01 13:32:32 2015 +0200
@@ -361,7 +361,7 @@
((Parse.position Parse.xname >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
- >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
+ >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
--| Parse.begin);
--- a/src/Pure/Isar/local_theory.ML Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML Wed Apr 01 13:32:32 2015 +0200
@@ -21,9 +21,6 @@
val assert_bottom: bool -> local_theory -> local_theory
val mark_brittle: local_theory -> local_theory
val assert_nonbrittle: local_theory -> local_theory
- val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
- local_theory -> local_theory
- val close_target: local_theory -> local_theory
val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val background_naming_of: local_theory -> Name_Space.naming
val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -73,6 +70,10 @@
val exit_global: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
+ val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+ local_theory -> Binding.scope * local_theory
+ val open_target: local_theory -> Binding.scope * local_theory
+ val close_target: local_theory -> local_theory
end;
structure Local_Theory: LOCAL_THEORY =
@@ -144,20 +145,6 @@
else lthy
end;
-fun open_target background_naming operations after_close lthy =
- let
- val _ = assert lthy;
- val (_, target) = Proof_Context.new_scope lthy;
- in
- target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
- end;
-
-fun close_target lthy =
- let
- val _ = assert_bottom false lthy;
- val ({after_close, ...} :: rest) = Data.get lthy;
- in lthy |> Data.put rest |> restore |> after_close end;
-
fun map_contexts f lthy =
let val n = level lthy in
lthy |> (Data.map o map_index)
@@ -350,18 +337,15 @@
-(** init and exit **)
+(** manage targets **)
-(* init *)
+(* outermost target *)
fun init background_naming operations target =
target |> Data.map
(fn [] => [make_lthy (background_naming, operations, I, false, target)]
| _ => error "Local theory already initialized");
-
-(* exit *)
-
val exit = operation #exit;
val exit_global = Proof_Context.theory_of o exit;
@@ -378,4 +362,25 @@
val phi = standard_morphism lthy thy_ctxt;
in (f phi x, thy) end;
+
+(* nested targets *)
+
+fun init_target background_naming operations after_close lthy =
+ let
+ val _ = assert lthy;
+ val (scope, target) = Proof_Context.new_scope lthy;
+ val lthy' =
+ target
+ |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+ in (scope, lthy') end;
+
+fun open_target lthy =
+ init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+
+fun close_target lthy =
+ let
+ val _ = assert_bottom false lthy;
+ val ({after_close, ...} :: rest) = Data.get lthy;
+ in lthy |> Data.put rest |> restore |> after_close end;
+
end;