src/Pure/Isar/local_theory.ML
changeset 28395 984fcc8feb24
parent 28379 0de8a35b866a
child 28406 daeb21fec18f
     1.1 --- a/src/Pure/Isar/local_theory.ML	Mon Sep 29 10:58:01 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Sep 29 10:58:03 2008 +0200
     1.3 @@ -42,6 +42,9 @@
     1.4    val restore: local_theory -> local_theory
     1.5    val reinit: local_theory -> local_theory
     1.6    val exit: local_theory -> Proof.context
     1.7 +  val exit_global: local_theory -> theory
     1.8 +  val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
     1.9 +  val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
    1.10  end;
    1.11  
    1.12  structure LocalTheory: LOCAL_THEORY =
    1.13 @@ -178,15 +181,14 @@
    1.14  fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
    1.15  
    1.16  fun target_morphism lthy =
    1.17 -  ProofContext.export_morphism lthy (target_of lthy) $>
    1.18 -  Morphism.thm_morphism Goal.norm_result;
    1.19 +  ProofContext.norm_export_morphism lthy (target_of lthy);
    1.20  
    1.21  fun notation add mode raw_args lthy =
    1.22    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    1.23    in term_syntax (ProofContext.target_notation add mode args) lthy end;
    1.24  
    1.25  
    1.26 -(* init -- exit *)
    1.27 +(* init *)
    1.28  
    1.29  fun init theory_prefix operations target = target |> Data.map
    1.30    (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
    1.31 @@ -198,6 +200,24 @@
    1.32    in init theory_prefix operations target end;
    1.33  
    1.34  val reinit = checkpoint o operation #reinit;
    1.35 +
    1.36 +
    1.37 +(* exit *)
    1.38 +
    1.39  val exit = ProofContext.theory Theory.checkpoint o operation #exit;
    1.40 +val exit_global = ProofContext.theory_of o exit;
    1.41 +
    1.42 +fun exit_result f (x, lthy) =
    1.43 +  let
    1.44 +    val ctxt = exit lthy;
    1.45 +    val phi = ProofContext.norm_export_morphism lthy ctxt;
    1.46 +  in (f phi x, ctxt) end;
    1.47 +
    1.48 +fun exit_result_global f (x, lthy) =
    1.49 +  let
    1.50 +    val thy = exit_global lthy;
    1.51 +    val thy_ctxt = ProofContext.init thy;
    1.52 +    val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
    1.53 +  in (f phi x, thy) end;
    1.54  
    1.55  end;