src/Pure/Isar/local_theory.ML
changeset 28379 0de8a35b866a
parent 28115 cd0d170d4dc6
child 28395 984fcc8feb24
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Sep 27 15:20:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Sep 27 15:20:39 2008 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val target_of: local_theory -> Proof.context
     1.5    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     1.6    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     1.7 +  val checkpoint: local_theory -> local_theory
     1.8    val full_naming: local_theory -> NameSpace.naming
     1.9    val full_name: local_theory -> bstring -> string
    1.10    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.11 @@ -131,6 +132,8 @@
    1.12  
    1.13  fun raw_theory f = #2 o raw_theory_result (f #> pair ());
    1.14  
    1.15 +val checkpoint = raw_theory Theory.checkpoint;
    1.16 +
    1.17  fun full_naming lthy =
    1.18    Sign.naming_of (ProofContext.theory_of lthy)
    1.19    |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
    1.20 @@ -165,12 +168,12 @@
    1.21  fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
    1.22  
    1.23  val pretty = operation #pretty;
    1.24 -val abbrev = operation2 #abbrev;
    1.25 -val define = operation2 #define;
    1.26 -val notes = operation2 #notes;
    1.27 -val type_syntax = operation1 #type_syntax;
    1.28 -val term_syntax = operation1 #term_syntax;
    1.29 -val declaration = operation1 #declaration;
    1.30 +val abbrev = apsnd checkpoint ooo operation2 #abbrev;
    1.31 +val define = apsnd checkpoint ooo operation2 #define;
    1.32 +val notes = apsnd checkpoint ooo operation2 #notes;
    1.33 +val type_syntax = checkpoint oo operation1 #type_syntax;
    1.34 +val term_syntax = checkpoint oo operation1 #term_syntax;
    1.35 +val declaration = checkpoint oo operation1 #declaration;
    1.36  
    1.37  fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
    1.38  
    1.39 @@ -187,13 +190,14 @@
    1.40  
    1.41  fun init theory_prefix operations target = target |> Data.map
    1.42    (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
    1.43 -    | SOME _ => error "Local theory already initialized");
    1.44 +    | SOME _ => error "Local theory already initialized")
    1.45 +  |> checkpoint;
    1.46  
    1.47  fun restore lthy =
    1.48    let val {group = _, theory_prefix, operations, target} = get_lthy lthy
    1.49    in init theory_prefix operations target end;
    1.50  
    1.51 -val reinit = operation #reinit;
    1.52 -val exit = operation #exit;
    1.53 +val reinit = checkpoint o operation #reinit;
    1.54 +val exit = ProofContext.theory Theory.checkpoint o operation #exit;
    1.55  
    1.56  end;