# HG changeset patch
# User wenzelm
# Date 1185212744 -7200
# Node ID 66e1f24d655ddadf869ddfa4981c7aa2fb2dd13a
# Parent  66923825628e9fce86aeef6b2c887476d44d8112
eliminated transform_failure (to avoid critical section for main transactions);

diff -r 66923825628e -r 66e1f24d655d src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Isar/antiquote.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -7,7 +7,6 @@
 
 signature ANTIQUOTE =
 sig
-  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
   datatype antiquote = Text of string | Antiq of string * Position.T
   val is_antiq: antiquote -> bool
   val scan_antiquotes: string * Position.T -> antiquote list
@@ -20,8 +19,6 @@
 
 (* datatype antiquote *)
 
-exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
-
 datatype antiquote =
   Text of string |
   Antiq of string * Position.T;
diff -r 66923825628e -r 66e1f24d655d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -14,7 +14,6 @@
 sig
   include BASIC_ATTRIB
   type src
-  exception ATTRIB_FAIL of (string * Position.T) * exn
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
@@ -87,8 +86,6 @@
 
 (* get attributes *)
 
-exception ATTRIB_FAIL of (string * Position.T) * exn;
-
 fun attribute_i thy =
   let
     val attrs = #2 (AttributesData.get thy);
@@ -96,7 +93,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup attrs name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME ((att, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (att src))
+        | SOME ((att, _), _) => att src)
       end;
   in attr end;
 
diff -r 66923825628e -r 66e1f24d655d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -69,7 +69,6 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> Position.T -> text
-  exception METHOD_FAIL of (string * Position.T) * exn
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method
   val add_methods: (bstring * (src -> Proof.context -> method) * string) list
@@ -406,8 +405,6 @@
 
 (* get methods *)
 
-exception METHOD_FAIL of (string * Position.T) * exn;
-
 fun method_i thy =
   let
     val meths = #2 (MethodsData.get thy);
@@ -415,7 +412,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup meths name of
           NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
-        | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
+        | SOME ((mth, _), _) => mth src)
       end;
   in meth end;
 
diff -r 66923825628e -r 66e1f24d655d src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -58,15 +58,11 @@
 
 (* apply print (ast) translation function *)
 
-fun apply_trans ctxt name a fns args =
+fun apply_trans ctxt fns args =
   let
     fun app_first [] = raise Match
       | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
-  in
-    transform_failure (fn Match => Match
-      | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
-      app_first fns
-  end;
+  in app_first fns end;
 
 fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
 
@@ -99,7 +95,7 @@
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of t
     and trans a args =
-      ast_of (apply_trans ctxt "print translation" a (apply_typed false dummyT (trf a)) args)
+      ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
@@ -160,7 +156,7 @@
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
     and trans a T args =
-      ast_of (apply_trans ctxt "print translation" a (apply_typed show_sorts T (trf a)) args)
+      ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
@@ -270,8 +266,6 @@
 
 fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   let
-    val trans = apply_trans ctxt "print ast translation";
-
     fun token_trans c [Ast.Variable x] =
           (case tokentrf c of
             NONE => NONE
@@ -359,7 +353,7 @@
         (case token_trans a args of     (*try token translation function*)
           SOME s => [Pretty.raw_str s]
         | NONE =>                       (*try print translation functions*)
-            astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
+            astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
       end
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
diff -r 66923825628e -r 66e1f24d655d src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -485,9 +485,7 @@
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
-      | SOME f => transform_failure (fn exn =>
-            EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))
-          (fn () => f ctxt args) ());
+      | SOME f => f ctxt args);
 
     (*translate pt bottom-up*)
     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
@@ -507,9 +505,7 @@
     fun trans a args =
       (case trf a of
         NONE => Term.list_comb (Lexicon.const a, args)
-      | SOME f => transform_failure (fn exn =>
-            EXCEPTION (exn, "Error in parse translation for " ^ quote a))
-          (fn () => f ctxt args) ());
+      | SOME f => f ctxt args);
 
     fun term_of (Ast.Constant a) = trans a []
       | term_of (Ast.Variable x) = Lexicon.read_var x
diff -r 66923825628e -r 66e1f24d655d src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/library.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -34,8 +34,6 @@
 
   (*exceptions*)
   exception EXCEPTION of exn * string
-  val do_transform_failure: bool ref
-  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
   datatype 'a result = Result of 'a | Exn of exn
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
@@ -273,13 +271,6 @@
 
 (* exceptions *)
 
-val do_transform_failure = ref true;
-
-fun transform_failure exn f x =
-  if ! do_transform_failure then
-    f x handle Interrupt => raise Interrupt | e => raise exn e
-  else f x;
-
 exception EXCEPTION of exn * string;
 
 datatype 'a result =