--- 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;
--- 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;
--- 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;
--- 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)
--- 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
--- 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 =