more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
authorwenzelm
Sat Jan 05 17:38:54 2013 +0100 (2013-01-05 ago)
changeset 507395165d7e6d3b9
parent 50738 d5725e56cd04
child 50740 21098a577294
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
explicit target for context within global theory with after_close = exit to manage the 2 levels involved here;
reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;
src/Pure/Isar/bundle.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/bundle.ML	Sat Jan 05 17:24:27 2013 +0100
     1.2 +++ b/src/Pure/Isar/bundle.ML	Sat Jan 05 17:38:54 2013 +0100
     1.3 @@ -93,20 +93,15 @@
     1.4  
     1.5  fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
     1.6    let
     1.7 -    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
     1.8 -    fun augment ctxt =
     1.9 -      let
    1.10 -        val ((_, _, _, ctxt'), _) = ctxt
    1.11 -          |> Context_Position.restore_visible lthy
    1.12 -          |> gen_includes prep_bundle raw_incls
    1.13 -          |> prep_decl ([], []) I raw_elems;
    1.14 -      in ctxt' |> Context_Position.restore_visible ctxt end;
    1.15 +    val (after_close, lthy) =
    1.16 +      gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
    1.17 +        (pair I o Local_Theory.assert);
    1.18 +    val ((_, _, _, lthy'), _) = lthy
    1.19 +      |> gen_includes prep_bundle raw_incls
    1.20 +      |> prep_decl ([], []) I raw_elems;
    1.21    in
    1.22 -    (case gthy of
    1.23 -      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
    1.24 -    | Context.Proof _ =>
    1.25 -        augment lthy |>
    1.26 -        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
    1.27 +    lthy' |> Local_Theory.open_target
    1.28 +      (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
    1.29    end;
    1.30  
    1.31  in
     2.1 --- a/src/Pure/Isar/local_theory.ML	Sat Jan 05 17:24:27 2013 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Jan 05 17:38:54 2013 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4    val restore: local_theory -> local_theory
     2.5    val level: Proof.context -> int
     2.6    val assert_bottom: bool -> local_theory -> local_theory
     2.7 -  val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
     2.8 +  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     2.9 +    local_theory -> local_theory
    2.10    val close_target: local_theory -> local_theory
    2.11    val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
    2.12    val naming_of: local_theory -> Name_Space.naming
    2.13 @@ -83,10 +84,11 @@
    2.14  type lthy =
    2.15   {naming: Name_Space.naming,
    2.16    operations: operations,
    2.17 +  after_close: local_theory -> local_theory,
    2.18    target: Proof.context};
    2.19  
    2.20 -fun make_lthy (naming, operations, target) : lthy =
    2.21 -  {naming = naming, operations = operations, target = target};
    2.22 +fun make_lthy (naming, operations, after_close, target) : lthy =
    2.23 +  {naming = naming, operations = operations, after_close = after_close, target = target};
    2.24  
    2.25  
    2.26  (* context data *)
    2.27 @@ -103,16 +105,17 @@
    2.28  val get_last_lthy = List.last o Data.get o assert;
    2.29  val get_first_lthy = hd o Data.get o assert;
    2.30  
    2.31 -fun map_first_lthy f = assert #>
    2.32 -  Data.map (fn {naming, operations, target} :: parents =>
    2.33 -    make_lthy (f (naming, operations, target)) :: parents);
    2.34 +fun map_first_lthy f =
    2.35 +  assert #>
    2.36 +  Data.map (fn {naming, operations, after_close, target} :: parents =>
    2.37 +    make_lthy (f (naming, operations, after_close, target)) :: parents);
    2.38  
    2.39  fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
    2.40  
    2.41  
    2.42  (* nested structure *)
    2.43  
    2.44 -val level = length o Data.get;
    2.45 +val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
    2.46  
    2.47  fun assert_bottom b lthy =
    2.48    let
    2.49 @@ -124,16 +127,20 @@
    2.50      else lthy
    2.51    end;
    2.52  
    2.53 -fun open_target naming operations target = assert target
    2.54 -  |> Data.map (cons (make_lthy (naming, operations, target)));
    2.55 +fun open_target naming operations after_close target =
    2.56 +  assert target
    2.57 +  |> Data.map (cons (make_lthy (naming, operations, after_close, target)));
    2.58  
    2.59  fun close_target lthy =
    2.60 -  assert_bottom false lthy |> Data.map tl |> restore;
    2.61 +  let
    2.62 +    val _ = assert_bottom false lthy;
    2.63 +    val {after_close, ...} :: rest = Data.get lthy;
    2.64 +  in lthy |> Data.put rest |> restore |> after_close end;
    2.65  
    2.66  fun map_contexts f lthy =
    2.67    let val n = level lthy in
    2.68 -    lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) =>
    2.69 -      make_lthy (naming, operations,
    2.70 +    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, target}) =>
    2.71 +      make_lthy (naming, operations, after_close,
    2.72          target
    2.73          |> Context_Position.set_visible false
    2.74          |> f (n - i - 1)
    2.75 @@ -148,7 +155,8 @@
    2.76  val full_name = Name_Space.full_name o naming_of;
    2.77  
    2.78  fun map_naming f =
    2.79 -  map_first_lthy (fn (naming, operations, target) => (f naming, operations, target));
    2.80 +  map_first_lthy (fn (naming, operations, after_close, target) =>
    2.81 +    (f naming, operations, after_close, target));
    2.82  
    2.83  val conceal = map_naming Name_Space.conceal;
    2.84  val new_group = map_naming Name_Space.new_group;
    2.85 @@ -279,7 +287,7 @@
    2.86  
    2.87  fun init naming operations target =
    2.88    target |> Data.map
    2.89 -    (fn [] => [make_lthy (naming, operations, target)]
    2.90 +    (fn [] => [make_lthy (naming, operations, I, target)]
    2.91        | _ => error "Local theory already initialized")
    2.92    |> checkpoint;
    2.93  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jan 05 17:24:27 2013 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jan 05 17:38:54 2013 +0100
     3.3 @@ -461,7 +461,13 @@
     3.4  val close_target = transaction (fn _ =>
     3.5    (fn Theory (Context.Proof lthy, _) =>
     3.6          (case try Local_Theory.close_target lthy of
     3.7 -          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
     3.8 +          SOME ctxt' =>
     3.9 +            let
    3.10 +              val gthy' =
    3.11 +                if can Local_Theory.assert ctxt'
    3.12 +                then Context.Proof ctxt'
    3.13 +                else Context.Theory (Proof_Context.theory_of ctxt');
    3.14 +            in Theory (gthy', SOME lthy) end
    3.15          | NONE => raise UNDEF)
    3.16      | _ => raise UNDEF));
    3.17