tuned signature;
authorwenzelm
Wed Apr 01 13:32:32 2015 +0200 (2015-04-01)
changeset 5989001aff5aa081d
parent 59889 30eef3e45bd0
child 59891 9ce697050455
tuned signature;
src/Pure/Isar/bundle.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/bundle.ML	Wed Apr 01 11:55:23 2015 +0200
     1.2 +++ b/src/Pure/Isar/bundle.ML	Wed Apr 01 13:32:32 2015 +0200
     1.3 @@ -20,9 +20,10 @@
     1.4    val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
     1.5    val including: string list -> Proof.state -> Proof.state
     1.6    val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
     1.7 -  val context: string list -> Element.context_i list -> generic_theory -> local_theory
     1.8 +  val context: string list -> Element.context_i list ->
     1.9 +    generic_theory -> Binding.scope * local_theory
    1.10    val context_cmd: (xstring * Position.T) list -> Element.context list ->
    1.11 -    generic_theory -> local_theory
    1.12 +    generic_theory -> Binding.scope * local_theory
    1.13    val print_bundles: Proof.context -> unit
    1.14  end;
    1.15  
    1.16 @@ -97,7 +98,7 @@
    1.17        |> gen_includes get raw_incls
    1.18        |> prep_decl ([], []) I raw_elems;
    1.19    in
    1.20 -    lthy' |> Local_Theory.open_target
    1.21 +    lthy' |> Local_Theory.init_target
    1.22        (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
    1.23    end;
    1.24  
    1.25 @@ -137,4 +138,3 @@
    1.26    end |> Pretty.writeln_chunks;
    1.27  
    1.28  end;
    1.29 -
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 11:55:23 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 13:32:32 2015 +0200
     2.3 @@ -361,7 +361,7 @@
     2.4      ((Parse.position Parse.xname >> (fn name =>
     2.5          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
     2.6        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
     2.7 -        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
     2.8 +        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
     2.9        --| Parse.begin);
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/local_theory.ML	Wed Apr 01 11:55:23 2015 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Apr 01 13:32:32 2015 +0200
     3.3 @@ -21,9 +21,6 @@
     3.4    val assert_bottom: bool -> local_theory -> local_theory
     3.5    val mark_brittle: local_theory -> local_theory
     3.6    val assert_nonbrittle: local_theory -> local_theory
     3.7 -  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     3.8 -    local_theory -> local_theory
     3.9 -  val close_target: local_theory -> local_theory
    3.10    val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
    3.11    val background_naming_of: local_theory -> Name_Space.naming
    3.12    val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
    3.13 @@ -73,6 +70,10 @@
    3.14    val exit_global: local_theory -> theory
    3.15    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
    3.16    val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
    3.17 +  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
    3.18 +    local_theory -> Binding.scope * local_theory
    3.19 +  val open_target: local_theory -> Binding.scope * local_theory
    3.20 +  val close_target: local_theory -> local_theory
    3.21  end;
    3.22  
    3.23  structure Local_Theory: LOCAL_THEORY =
    3.24 @@ -144,20 +145,6 @@
    3.25      else lthy
    3.26    end;
    3.27  
    3.28 -fun open_target background_naming operations after_close lthy =
    3.29 -  let
    3.30 -    val _ = assert lthy;
    3.31 -    val (_, target) = Proof_Context.new_scope lthy;
    3.32 -  in
    3.33 -    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
    3.34 -  end;
    3.35 -
    3.36 -fun close_target lthy =
    3.37 -  let
    3.38 -    val _ = assert_bottom false lthy;
    3.39 -    val ({after_close, ...} :: rest) = Data.get lthy;
    3.40 -  in lthy |> Data.put rest |> restore |> after_close end;
    3.41 -
    3.42  fun map_contexts f lthy =
    3.43    let val n = level lthy in
    3.44      lthy |> (Data.map o map_index)
    3.45 @@ -350,18 +337,15 @@
    3.46  
    3.47  
    3.48  
    3.49 -(** init and exit **)
    3.50 +(** manage targets **)
    3.51  
    3.52 -(* init *)
    3.53 +(* outermost target *)
    3.54  
    3.55  fun init background_naming operations target =
    3.56    target |> Data.map
    3.57      (fn [] => [make_lthy (background_naming, operations, I, false, target)]
    3.58        | _ => error "Local theory already initialized");
    3.59  
    3.60 -
    3.61 -(* exit *)
    3.62 -
    3.63  val exit = operation #exit;
    3.64  val exit_global = Proof_Context.theory_of o exit;
    3.65  
    3.66 @@ -378,4 +362,25 @@
    3.67      val phi = standard_morphism lthy thy_ctxt;
    3.68    in (f phi x, thy) end;
    3.69  
    3.70 +
    3.71 +(* nested targets *)
    3.72 +
    3.73 +fun init_target background_naming operations after_close lthy =
    3.74 +  let
    3.75 +    val _ = assert lthy;
    3.76 +    val (scope, target) = Proof_Context.new_scope lthy;
    3.77 +    val lthy' =
    3.78 +      target
    3.79 +      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
    3.80 +  in (scope, lthy') end;
    3.81 +
    3.82 +fun open_target lthy =
    3.83 +  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
    3.84 +
    3.85 +fun close_target lthy =
    3.86 +  let
    3.87 +    val _ = assert_bottom false lthy;
    3.88 +    val ({after_close, ...} :: rest) = Data.get lthy;
    3.89 +  in lthy |> Data.put rest |> restore |> after_close end;
    3.90 +
    3.91  end;