src/Pure/Isar/toplevel.ML
changeset 59923 b21c82422d65
parent 59472 513300fa2d09
child 59939 7d46aa03696e
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Apr 03 21:25:55 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Apr 04 14:04:11 2015 +0200
     1.3 @@ -51,15 +51,15 @@
     1.4    val end_local_theory: transition -> transition
     1.5    val open_target: (generic_theory -> local_theory) -> transition -> transition
     1.6    val close_target: transition -> transition
     1.7 -  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
     1.8 -    transition -> transition
     1.9 -  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
    1.10 -    transition -> transition
    1.11 +  val local_theory': Position.T option -> (xstring * Position.T) option ->
    1.12 +    (bool -> local_theory -> local_theory) -> transition -> transition
    1.13 +  val local_theory: Position.T option -> (xstring * Position.T) option ->
    1.14 +    (local_theory -> local_theory) -> transition -> transition
    1.15    val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
    1.16      transition -> transition
    1.17 -  val local_theory_to_proof': (xstring * Position.T) option ->
    1.18 +  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
    1.19      (bool -> local_theory -> Proof.state) -> transition -> transition
    1.20 -  val local_theory_to_proof: (xstring * Position.T) option ->
    1.21 +  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
    1.22      (local_theory -> Proof.state) -> transition -> transition
    1.23    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    1.24    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    1.25 @@ -412,11 +412,12 @@
    1.26          | NONE => raise UNDEF)
    1.27      | _ => raise UNDEF));
    1.28  
    1.29 -fun local_theory' loc f = present_transaction (fn int =>
    1.30 +fun local_theory' private target f = present_transaction (fn int =>
    1.31    (fn Theory (gthy, _) =>
    1.32          let
    1.33 -          val (finish, lthy) = Named_Target.switch loc gthy;
    1.34 +          val (finish, lthy) = Named_Target.switch target gthy;
    1.35            val lthy' = lthy
    1.36 +            |> fold Proof_Context.private (the_list private)
    1.37              |> Local_Theory.new_group
    1.38              |> f int
    1.39              |> Local_Theory.reset_group;
    1.40 @@ -424,11 +425,11 @@
    1.41      | _ => raise UNDEF))
    1.42    (K ());
    1.43  
    1.44 -fun local_theory loc f = local_theory' loc (K f);
    1.45 +fun local_theory private target f = local_theory' private target (K f);
    1.46  
    1.47 -fun present_local_theory loc = present_transaction (fn int =>
    1.48 +fun present_local_theory target = present_transaction (fn int =>
    1.49    (fn Theory (gthy, _) =>
    1.50 -        let val (finish, lthy) = Named_Target.switch loc gthy;
    1.51 +        let val (finish, lthy) = Named_Target.switch target gthy;
    1.52          in Theory (finish lthy, SOME lthy) end
    1.53      | _ => raise UNDEF));
    1.54  
    1.55 @@ -469,12 +470,18 @@
    1.56  
    1.57  in
    1.58  
    1.59 -fun local_theory_to_proof' loc f = begin_proof
    1.60 +fun local_theory_to_proof' private target f = begin_proof
    1.61    (fn int => fn gthy =>
    1.62 -    let val (finish, lthy) = Named_Target.switch loc gthy
    1.63 -    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    1.64 +    let
    1.65 +      val (finish, lthy) = Named_Target.switch target gthy;
    1.66 +      val prf = lthy
    1.67 +        |> fold Proof_Context.private (the_list private)
    1.68 +        |> Local_Theory.new_group
    1.69 +        |> f int;
    1.70 +    in (finish o Local_Theory.reset_group, prf) end);
    1.71  
    1.72 -fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    1.73 +fun local_theory_to_proof private target f =
    1.74 +  local_theory_to_proof' private target (K f);
    1.75  
    1.76  fun theory_to_proof f = begin_proof
    1.77    (fn _ => fn gthy =>