src/Pure/Isar/toplevel.ML
changeset 59939 7d46aa03696e
parent 59923 b21c82422d65
child 59990 a81dc82ecba3
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Apr 06 22:11:01 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': Position.T option -> (xstring * Position.T) option ->
     1.8 +  val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
     1.9      (bool -> local_theory -> local_theory) -> transition -> transition
    1.10 -  val local_theory: Position.T option -> (xstring * Position.T) option ->
    1.11 +  val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
    1.12      (local_theory -> local_theory) -> transition -> transition
    1.13    val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
    1.14      transition -> transition
    1.15 -  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
    1.16 +  val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
    1.17      (bool -> local_theory -> Proof.state) -> transition -> transition
    1.18 -  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
    1.19 +  val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option ->
    1.20      (local_theory -> Proof.state) -> transition -> transition
    1.21    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    1.22    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    1.23 @@ -412,12 +412,15 @@
    1.24          | NONE => raise UNDEF)
    1.25      | _ => raise UNDEF));
    1.26  
    1.27 -fun local_theory' private target f = present_transaction (fn int =>
    1.28 +val limited_context =
    1.29 +  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
    1.30 +
    1.31 +fun local_theory' limited target f = present_transaction (fn int =>
    1.32    (fn Theory (gthy, _) =>
    1.33          let
    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 +            |> limited_context limited
    1.38              |> Local_Theory.new_group
    1.39              |> f int
    1.40              |> Local_Theory.reset_group;
    1.41 @@ -425,7 +428,7 @@
    1.42      | _ => raise UNDEF))
    1.43    (K ());
    1.44  
    1.45 -fun local_theory private target f = local_theory' private target (K f);
    1.46 +fun local_theory limited target f = local_theory' limited target (K f);
    1.47  
    1.48  fun present_local_theory target = present_transaction (fn int =>
    1.49    (fn Theory (gthy, _) =>
    1.50 @@ -470,18 +473,18 @@
    1.51  
    1.52  in
    1.53  
    1.54 -fun local_theory_to_proof' private target f = begin_proof
    1.55 +fun local_theory_to_proof' limited target f = begin_proof
    1.56    (fn int => fn gthy =>
    1.57      let
    1.58        val (finish, lthy) = Named_Target.switch target gthy;
    1.59        val prf = lthy
    1.60 -        |> fold Proof_Context.private (the_list private)
    1.61 +        |> limited_context limited
    1.62          |> Local_Theory.new_group
    1.63          |> f int;
    1.64      in (finish o Local_Theory.reset_group, prf) end);
    1.65  
    1.66 -fun local_theory_to_proof private target f =
    1.67 -  local_theory_to_proof' private target (K f);
    1.68 +fun local_theory_to_proof limited target f =
    1.69 +  local_theory_to_proof' limited target (K f);
    1.70  
    1.71  fun theory_to_proof f = begin_proof
    1.72    (fn _ => fn gthy =>