src/Pure/Isar/local_theory.ML
changeset 59890 01aff5aa081d
parent 59887 43dc3c660f41
child 61111 2618e7e3b5ea
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Apr 01 11:55:23 2015 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Apr 01 13:32:32 2015 +0200
     1.3 @@ -21,9 +21,6 @@
     1.4    val assert_bottom: bool -> local_theory -> local_theory
     1.5    val mark_brittle: local_theory -> local_theory
     1.6    val assert_nonbrittle: local_theory -> local_theory
     1.7 -  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     1.8 -    local_theory -> local_theory
     1.9 -  val close_target: local_theory -> local_theory
    1.10    val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
    1.11    val background_naming_of: local_theory -> Name_Space.naming
    1.12    val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
    1.13 @@ -73,6 +70,10 @@
    1.14    val exit_global: local_theory -> theory
    1.15    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
    1.16    val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
    1.17 +  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
    1.18 +    local_theory -> Binding.scope * local_theory
    1.19 +  val open_target: local_theory -> Binding.scope * local_theory
    1.20 +  val close_target: local_theory -> local_theory
    1.21  end;
    1.22  
    1.23  structure Local_Theory: LOCAL_THEORY =
    1.24 @@ -144,20 +145,6 @@
    1.25      else lthy
    1.26    end;
    1.27  
    1.28 -fun open_target background_naming operations after_close lthy =
    1.29 -  let
    1.30 -    val _ = assert lthy;
    1.31 -    val (_, target) = Proof_Context.new_scope lthy;
    1.32 -  in
    1.33 -    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
    1.34 -  end;
    1.35 -
    1.36 -fun close_target lthy =
    1.37 -  let
    1.38 -    val _ = assert_bottom false lthy;
    1.39 -    val ({after_close, ...} :: rest) = Data.get lthy;
    1.40 -  in lthy |> Data.put rest |> restore |> after_close end;
    1.41 -
    1.42  fun map_contexts f lthy =
    1.43    let val n = level lthy in
    1.44      lthy |> (Data.map o map_index)
    1.45 @@ -350,18 +337,15 @@
    1.46  
    1.47  
    1.48  
    1.49 -(** init and exit **)
    1.50 +(** manage targets **)
    1.51  
    1.52 -(* init *)
    1.53 +(* outermost target *)
    1.54  
    1.55  fun init background_naming operations target =
    1.56    target |> Data.map
    1.57      (fn [] => [make_lthy (background_naming, operations, I, false, target)]
    1.58        | _ => error "Local theory already initialized");
    1.59  
    1.60 -
    1.61 -(* exit *)
    1.62 -
    1.63  val exit = operation #exit;
    1.64  val exit_global = Proof_Context.theory_of o exit;
    1.65  
    1.66 @@ -378,4 +362,25 @@
    1.67      val phi = standard_morphism lthy thy_ctxt;
    1.68    in (f phi x, thy) end;
    1.69  
    1.70 +
    1.71 +(* nested targets *)
    1.72 +
    1.73 +fun init_target background_naming operations after_close lthy =
    1.74 +  let
    1.75 +    val _ = assert lthy;
    1.76 +    val (scope, target) = Proof_Context.new_scope lthy;
    1.77 +    val lthy' =
    1.78 +      target
    1.79 +      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
    1.80 +  in (scope, lthy') end;
    1.81 +
    1.82 +fun open_target lthy =
    1.83 +  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
    1.84 +
    1.85 +fun close_target lthy =
    1.86 +  let
    1.87 +    val _ = assert_bottom false lthy;
    1.88 +    val ({after_close, ...} :: rest) = Data.get lthy;
    1.89 +  in lthy |> Data.put rest |> restore |> after_close end;
    1.90 +
    1.91  end;