# HG changeset patch
# User wenzelm
# Date 926969507 -7200
# Node ID 6e17d06007d2096cd717f33a727bc74d19e2cd75
# Parent  7a056250899d9afaa916bf172493ecb2d7529a9d
backup operation replaces transaction;

diff -r 7a056250899d -r 6e17d06007d2 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon May 17 21:31:08 1999 +0200
+++ b/src/Pure/pure_thy.ML	Mon May 17 21:31:47 1999 +0200
@@ -48,8 +48,7 @@
   val local_path: theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
-  exception ROLLBACK of theory * exn option
-  val transaction: (theory -> theory) -> theory -> theory
+  val backup: theory -> theory
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   val dummy_patternN: string
 end;
@@ -325,9 +324,9 @@
 structure TheoryManagementDataArgs =
 struct
   val name = "Pure/theory_management";
-  type T = {name: string, generation: int};
+  type T = {name: string, version: int};
 
-  val empty = {name = "", generation = 0};
+  val empty = {name = "", version = 0};
   val copy = I;
   val prep_ext  = I;
   fun merge _ = empty;
@@ -342,7 +341,7 @@
 (* get / put name *)
 
 val get_name = #name o get_info;
-fun put_name name = put_info {name = name, generation = 0};
+fun put_name name = put_info {name = name, version = 0};
 
 
 (* control prefixing of theory name *)
@@ -363,22 +362,14 @@
 fun end_theory thy = Theory.add_name (get_name thy) thy;
 
 
-(* atomic transactions *)
-
-exception ROLLBACK of theory * exn option;
+(* make backup copy *)
 
-fun transaction f thy =
-  let
-    val {name, generation} = get_info thy;
-    val copy_thy =
-      thy
-      |> Theory.copy
-      |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
-      |> put_info {name = name, generation = generation + 1};
-    val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);
-  in
-    if Sign.is_stale (Theory.sign_of thy') then raise ROLLBACK (copy_thy, opt_exn)
-    else (case opt_exn of Some exn => raise exn | _ => thy')
+fun backup thy =
+  let val {name, version} = get_info thy in
+    thy
+    |> Theory.prep_ext
+    |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int version)
+    |> put_info {name = name, version = version + 1}
   end;