--- a/TFL/casesplit.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/TFL/casesplit.ML Sat Jan 14 17:14:06 2006 +0100
@@ -100,13 +100,11 @@
val dtypestab = DatatypePackage.get_datatypes sgn;
val ty_str = case ty of
Type(ty_str, _) => ty_str
- | TFree(s,_) => raise ERROR_MESSAGE
- ("Free type: " ^ s)
- | TVar((s,i),_) => raise ERROR_MESSAGE
- ("Free variable: " ^ s)
+ | TFree(s,_) => error ("Free type: " ^ s)
+ | TVar((s,i),_) => error ("Free variable: " ^ s)
val dt = case Symtab.lookup dtypestab ty_str
of SOME dt => dt
- | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str)
+ | NONE => error ("Not a Datatype: " ^ ty_str)
in
cases_thm_of_induct_thm (#induction dt)
end;
@@ -138,7 +136,7 @@
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
(Pv, Dv,
Sign.typ_match sgn (Dty, ty) Vartab.empty)
- | _ => raise ERROR_MESSAGE ("not a valid case thm");
+ | _ => error "not a valid case thm";
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
(Vartab.dest type_insts);
val cPv = ctermify (Envir.subst_TVars type_insts Pv);
@@ -187,7 +185,7 @@
end;
val (n,ty) = case Library.get_first getter freets
of SOME (n, ty) => (n, ty)
- | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr);
+ | _ => error ("no such variable " ^ vstr);
val sgn = Thm.sign_of_thm th;
val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
@@ -284,7 +282,7 @@
(writeln "th:";
Display.print_thm th; writeln "split ths:";
Display.print_thms splitths; writeln "\n--";
- raise ERROR_MESSAGE "splitto: cannot find variable to split on")
+ error "splitto: cannot find variable to split on")
| SOME v =>
let
val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
@@ -321,7 +319,7 @@
fun add_eq (i, e) xs =
(e, (get_related_thms i rules), i) :: xs
fun solve_eq (th, [], i) =
- raise ERROR_MESSAGE "derive_init_eqs: missing rules"
+ error "derive_init_eqs: missing rules"
| solve_eq (th, [a], i) = (a, i)
| solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
val eqths =
--- a/TFL/post.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/TFL/post.ML Sat Jan 14 17:14:06 2006 +0100
@@ -207,7 +207,7 @@
List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
fun solve_eq (th, [], i) =
- raise ERROR_MESSAGE "derive_init_eqs: missing rules"
+ error "derive_init_eqs: missing rules"
| solve_eq (th, [a], i) = [(a, i)]
| solve_eq (th, splitths as (_ :: _), i) =
(writeln "Proving unsplit equation...";
@@ -215,7 +215,7 @@
(CaseSplit.splitto splitths th), i)])
(* if there's an error, pretend nothing happened with this definition
We should probably print something out so that the user knows...? *)
- handle ERROR_MESSAGE s =>
+ handle ERROR s =>
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
in
fun derive_init_eqs sgn rules eqs =
--- a/TFL/rules.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/TFL/rules.ML Sat Jan 14 17:14:06 2006 +0100
@@ -819,7 +819,7 @@
val result =
if strict then Goal.prove thy [] [] t (K tac)
else Goal.prove thy [] [] t (K tac)
- handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
+ handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
in #1 (freeze_thaw (standard result)) end;
end;
--- a/TFL/tfl.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/TFL/tfl.ML Sat Jan 14 17:14:06 2006 +0100
@@ -578,7 +578,7 @@
val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
theory Hilbert_Choice*)
thm "Hilbert_Choice.tfl_some"
- handle ERROR => error
+ handle ERROR msg => cat_error msg
"defer_recdef requires theory Main or at least Hilbert_Choice as parent"
val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
in {theory = theory, R=R1, SV=SV,
--- a/src/CTT/ex/elim.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/CTT/ex/elim.ML Sat Jan 14 17:14:06 2006 +0100
@@ -20,7 +20,7 @@
result();
writeln"first solution is fst; backtracking gives snd";
back();
-back() handle ERROR => writeln"And there are indeed no others";
+back() handle ERROR _ => writeln"And there are indeed no others";
writeln"Double negation of the Excluded Middle";
--- a/src/FOL/ex/IffOracle.thy Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOL/ex/IffOracle.thy Sat Jan 14 17:14:06 2006 +0100
@@ -40,12 +40,12 @@
text {* These oracle calls had better fail *}
ML {*
- (iff_oracle (the_context ()) 5; raise ERROR)
+ (iff_oracle (the_context ()) 5; error "?")
handle Fail _ => warning "Oracle failed, as expected"
*}
ML {*
- (iff_oracle (the_context ()) 1; raise ERROR)
+ (iff_oracle (the_context ()) 1; error "?")
handle Fail _ => warning "Oracle failed, as expected"
*}
--- a/src/FOL/ex/foundn.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOL/ex/foundn.ML Sat Jan 14 17:14:06 2006 +0100
@@ -92,7 +92,7 @@
goal IFOL.thy "EX y. ALL x. x=y";
by (rtac exI 1);
by (rtac allI 1);
-by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
+by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/FOL/ex/int.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOL/ex/int.ML Sat Jan 14 17:14:06 2006 +0100
@@ -84,12 +84,12 @@
(*The attempt to prove them terminates quickly!*)
Goal "((P-->Q) --> P) --> P";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
Goal "(P&Q-->R) --> (P-->R) | (Q-->R)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
@@ -272,24 +272,24 @@
(*The attempt to prove them terminates quickly!*)
Goal "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
Goal "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
Goal "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
Goal "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
(*Classically but not intuitionistically valid. Proved by a bug in 1986!*)
Goal "EX x. Q(x) --> (ALL x. Q(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/FOL/ex/quant.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOL/ex/quant.ML Sat Jan 14 17:14:06 2006 +0100
@@ -62,22 +62,22 @@
writeln"The following should fail, as they are false!";
Goal "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
Goal "(EX x. Q(x)) --> (ALL x. Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
Goal "P(?a) --> (ALL x. P(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
Goal
"(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/FOLP/ex/foundn.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOLP/ex/foundn.ML Sat Jan 14 17:14:06 2006 +0100
@@ -92,7 +92,7 @@
goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
by (rtac exI 1);
by (rtac allI 1);
-by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
+by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/FOLP/ex/int.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOLP/ex/int.ML Sat Jan 14 17:14:06 2006 +0100
@@ -63,12 +63,12 @@
(*The attempt to prove them terminates quickly!*)
goal (theory "IFOLP") "?p : ((P-->Q) --> P) --> P";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
goal (theory "IFOLP") "?p : (P&Q-->R) --> (P-->R) | (Q-->R)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
@@ -205,24 +205,24 @@
(*The attempt to prove them terminates quickly!*)
goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
(*Classically but not intuitionistically valid. Proved by a bug in 1986!*)
goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
-by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/FOLP/ex/quant.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOLP/ex/quant.ML Sat Jan 14 17:14:06 2006 +0100
@@ -60,22 +60,22 @@
writeln"The following should fail, as they are false!";
Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
Goal "?p : P(?a) --> (ALL x. P(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
Goal
"?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/HOL/Import/proof_kernel.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sat Jan 14 17:14:06 2006 +0100
@@ -212,17 +212,17 @@
fun F n =
let
val str = Library.setmp show_brackets false (G n string_of_cterm) ct
- val cu = transform_error (read_cterm sign) (str,T)
+ val cu = read_cterm sign (str,T)
in
if match cu
then quote str
else F (n+1)
end
- handle ERROR_MESSAGE mesg => F (n+1)
+ handle ERROR mesg => F (n+1)
in
- transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F)) 0
+ Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
- handle ERROR_MESSAGE mesg => simple_smart_string_of_cterm ct
+ handle ERROR mesg => simple_smart_string_of_cterm ct
val smart_string_of_thm = smart_string_of_cterm o cprop_of
@@ -457,11 +457,13 @@
fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
-fun handle_error f d = transform_error f () handle ERROR_MESSAGE _ => d
+val check_name_thy = theory "Main"
-val check_name_thy = theory "Main"
-fun valid_boundvarname s = handle_error (fn () => (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true)) false
-fun valid_varname s = handle_error (fn () => (read_cterm check_name_thy (s, TypeInfer.logicT); true)) false
+fun valid_boundvarname s =
+ can (fn () => read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
+
+fun valid_varname s =
+ can (fn () => read_cterm check_name_thy (s, TypeInfer.logicT)) ();
fun protect_varname s =
if innocent_varname s andalso valid_varname s then s else
@@ -1253,8 +1255,8 @@
case get_hol4_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
- val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
- handle ERROR_MESSAGE _ =>
+ val th1 = (SOME (PureThy.get_thm thy (Name thmname))
+ handle ERROR _ =>
(case split_name thmname of
SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
handle _ => NONE)
@@ -2123,7 +2125,8 @@
fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
case HOL4DefThy.get thy of
- Replaying _ => (thy, handle_error (fn () => HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern")))) hth)
+ Replaying _ => (thy,
+ HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
| _ =>
let
val _ = message "TYPE_INTRO:"
--- a/src/HOL/Tools/datatype_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -976,8 +976,8 @@
Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
- end handle ERROR =>
- error ("The error above occured in constructor " ^ cname ^
+ end handle ERROR msg =>
+ cat_error msg ("The error above occured in constructor " ^ cname ^
" of datatype " ^ tname);
val (constrs', constr_syntax', sorts') =
--- a/src/HOL/Tools/inductive_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -850,7 +850,7 @@
val intr_names = map (fst o fst) intro_srcs;
fun read_rule s = Thm.read_cterm thy (s, propT)
- handle ERROR => error ("The error(s) above occurred for " ^ s);
+ handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
val (cs', intr_ts') = unify_consts thy cs intr_ts;
--- a/src/HOL/Tools/primrec_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -272,7 +272,7 @@
val ((names, strings), srcss) = apfst split_list (split_list eqns);
val atts = map (map (Attrib.global_attribute thy)) srcss;
val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT))
- handle ERROR => error ("The error(s) above occurred for " ^ s)) strings;
+ handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts;
val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts
--- a/src/HOL/Tools/record_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -2024,7 +2024,7 @@
fun prep_inst T = snd (cert_typ sign ([], T));
val parent = Option.map (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
- handle ERROR => error ("The error(s) above in parent record specification");
+ handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
val parents = add_parents thy parent [];
val init_env =
@@ -2036,8 +2036,8 @@
(* fields *)
fun prep_field (env, (c, raw_T, mx)) =
- let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
- error ("The error(s) above occured in field " ^ quote c)
+ let val (env', T) = prep_typ sign (env, raw_T) handle ERROR msg =>
+ cat_error msg ("The error(s) above occured in field " ^ quote c)
in (env', (c, T, mx)) end;
val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
@@ -2090,7 +2090,7 @@
if null errs then () else error (cat_lines errs) ;
thy |> record_definition (args, bname) parent parents bfields
end
- handle ERROR => error ("Failed to define record " ^ quote bname);
+ handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);
val add_record = gen_add_record read_typ read_raw_parent;
val add_record_i = gen_add_record cert_typ (K I);
--- a/src/HOL/Tools/refute.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/refute.ML Sat Jan 14 17:14:06 2006 +0100
@@ -466,7 +466,7 @@
case Type.lookup (typeSubs, v) of
NONE =>
(* schematic type variable not instantiated *)
- raise ERROR
+ error ""
| SOME typ =>
typ)) t
(* Term.term list * Term.typ -> Term.term list *)
@@ -550,7 +550,7 @@
| NONE =>
get_typedefn axms
end
- handle ERROR => get_typedefn axms
+ handle ERROR _ => get_typedefn axms
| MATCH => get_typedefn axms
| Type.TYPE_MATCH => get_typedefn axms)
in
@@ -650,7 +650,7 @@
else
get_defn axms
end
- handle ERROR => get_defn axms
+ handle ERROR _ => get_defn axms
| TERM _ => get_defn axms
| Type.TYPE_MATCH => get_defn axms)
(* axiomatic type classes *)
--- a/src/HOL/Tools/sat_solver.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/sat_solver.ML Sat Jan 14 17:14:06 2006 +0100
@@ -307,7 +307,7 @@
[] => [xs1]
| (0::[]) => [xs1]
| (0::tl) => xs1 :: clauses tl
- | _ => raise ERROR (* this cannot happen *)
+ | _ => sys_error "this cannot happen"
end
(* int -> PropLogic.prop_formula *)
fun literal_from_int i =
@@ -457,7 +457,7 @@
| forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2)
(* Above, i *and* ~i may be forced. In this case the first occurrence takes *)
(* precedence, and the next partial evaluation of the formula returns 'False'. *)
- | forced_vars _ = raise ERROR (* formula is not in negation normal form *)
+ | forced_vars _ = error "formula is not in negation normal form"
(* int list -> prop_formula -> (int list * prop_formula) *)
fun eval_and_force xs fm =
let
@@ -528,7 +528,7 @@
(if name="dpll" orelse name="enumerate" then
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
else
- debug ("Using SAT solver " ^ quote name ^ "."));
+ Output.debug ("Using SAT solver " ^ quote name ^ "."));
(* apply 'solver' to 'fm' *)
solver fm
handle SatSolver.NOT_CONFIGURED => loop solvers
--- a/src/HOL/Tools/typedef_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -93,8 +93,8 @@
fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
-fun err_in_typedef name =
- error ("The error(s) above occurred in typedef " ^ quote name);
+fun err_in_typedef msg name =
+ cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
let
@@ -224,7 +224,7 @@
setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
in (cset, goal, goal_pat, typedef_result) end
- handle ERROR => err_in_typedef name;
+ handle ERROR msg => err_in_typedef msg name;
(* add_typedef interfaces *)
@@ -237,8 +237,8 @@
val (cset, goal, _, typedef_result) =
prepare_typedef prep_term def name typ set opt_morphs thy;
val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
- val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
- error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
+ val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
+ cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
val ((thy', _), result) = (thy, non_empty) |> typedef_result;
in (thy', result) end;
--- a/src/HOL/ex/ROOT.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/ex/ROOT.ML Sat Jan 14 17:14:06 2006 +0100
@@ -45,7 +45,7 @@
if_svc_enabled time_use_thy "svc_test";
(* requires zChaff with proof generation to be installed: *)
-time_use_thy "SAT_Examples" handle ERROR => ();
+try time_use_thy "SAT_Examples";
(* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
if getenv "ZCHAFF_HOME" <> "" then
--- a/src/HOLCF/adm_tac.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOLCF/adm_tac.ML Sat Jan 14 17:14:06 2006 +0100
@@ -104,7 +104,7 @@
val t' = mk_all params (Logic.list_implies (prems, t));
val thm = Goal.prove sign [] [] t' (K (tac 1));
in (ts, thm)::l end
- handle ERROR_MESSAGE _ => l;
+ handle ERROR _ => l;
(*** instantiation of adm_subst theorem (a bit tricky) ***)
--- a/src/HOLCF/cont_consts.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOLCF/cont_consts.ML Sat Jan 14 17:14:06 2006 +0100
@@ -72,7 +72,7 @@
fun is_contconst (_,_,NoSyn ) = false
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
- handle ERROR => error ("in mixfix annotation for " ^
+ handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
quote (Syntax.const_name c mx));
--- a/src/HOLCF/domain/theorems.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Jan 14 17:14:06 2006 +0100
@@ -587,7 +587,7 @@
strip_tac 1,
rtac (rewrite_rule axs_take_def finite_ind) 1,
ind_prems_tac prems])
- handle ERROR => (warning "Cannot prove infinite induction rule"; refl))
+ handle ERROR _ => (warning "Cannot prove infinite induction rule"; refl))
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
--- a/src/HOLCF/pcpodef_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -53,8 +53,8 @@
fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
-fun err_in_cpodef name =
- error ("The error(s) above occurred in cpodef " ^ quote name);
+fun err_in_cpodef msg name =
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
@@ -168,7 +168,7 @@
end;
in (goal, if pcpo then pcpodef_result else cpodef_result) end
- handle ERROR => err_in_cpodef name;
+ handle ERROR msg => err_in_cpodef msg name;
(* cpodef_proof interface *)
--- a/src/Provers/induct_method.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Provers/induct_method.ML Sat Jan 14 17:14:06 2006 +0100
@@ -53,11 +53,11 @@
fun align_left msg xs ys =
let val m = length xs and n = length ys
- in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
+ in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
fun align_right msg xs ys =
let val m = length xs and n = length ys
- in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
+ in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
(* prep_inst *)
@@ -72,7 +72,7 @@
val ct = cert (tune t);
in
if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
- else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
+ else error (Pretty.string_of (Pretty.block
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
--- a/src/Pure/General/file.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/General/file.ML Sat Jan 14 17:14:06 2006 +0100
@@ -147,6 +147,6 @@
(* use ML files *)
-val use = use o platform_path;
+val use = Output.toplevel_errors (use o platform_path);
end;
--- a/src/Pure/IsaPlanner/isand.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/IsaPlanner/isand.ML Sat Jan 14 17:14:06 2006 +0100
@@ -324,8 +324,7 @@
(* lookup type of a free var name from a list *)
fun lookupfree vs vn =
case Library.find_first (fn (n,ty) => n = vn) vs of
- NONE => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: "
- ^ vn ^ " does not occur in the term")
+ NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
| SOME x => x;
in
fun export_back (export {fixes = vs, assumes = hprems,
@@ -523,7 +522,7 @@
val t = (prop_of th);
val gt = Logic.get_goal t i;
val _ = case Term.strip_all_vars gt of [] => ()
- | _ => raise ERROR_MESSAGE "assume_prems: goal has params"
+ | _ => error "assume_prems: goal has params"
val body = gt;
val prems = Logic.strip_imp_prems body;
val concl = Logic.strip_imp_concl body;
--- a/src/Pure/Isar/attrib.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Jan 14 17:14:06 2006 +0100
@@ -171,7 +171,7 @@
at the thm structure.*)
fun crude_closure ctxt src =
- (try (transform_error (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl))) ();
+ (try (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl)) ();
Args.closure src);
--- a/src/Pure/Isar/calculation.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/calculation.ML Sat Jan 14 17:14:06 2006 +0100
@@ -109,7 +109,7 @@
(** proof commands **)
-fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
+fun err_if b msg = if b then error msg else ();
fun assert_sane final =
if final then Proof.assert_forward else Proof.assert_forward_or_chain;
@@ -147,8 +147,8 @@
NONE => (true, Seq.single facts)
| SOME calc => (false, Seq.map single (combine (calc @ facts))));
in
- err_if state (initial andalso final) "No calculation yet";
- err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
+ err_if (initial andalso final) "No calculation yet";
+ err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
state |> maintain_calculation final calc))
end;
@@ -170,7 +170,7 @@
| SOME thms => (false, thms));
val calc = thms @ facts;
in
- err_if state (initial andalso final) "No calculation yet";
+ err_if (initial andalso final) "No calculation yet";
print_calculation int (Proof.context_of state) calc;
state |> maintain_calculation final calc
end;
--- a/src/Pure/Isar/isar_output.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML Sat Jan 14 17:14:06 2006 +0100
@@ -144,8 +144,10 @@
in
fun antiq_args lex (s, pos) =
- (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
- error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
+ let
+ fun err msg = cat_error msg
+ ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
+ in (case antiq_args_aux lex (s, pos) of [x] => x | _ => err "") handle ERROR msg => err msg end;
end;
--- a/src/Pure/Isar/isar_thy.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/isar_thy.ML Sat Jan 14 17:14:06 2006 +0100
@@ -134,8 +134,8 @@
(* global endings *)
fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
- (Proof.assert_bottom true state handle Proof.STATE _ => raise Toplevel.UNDEF;
- ending int state));
+ if can (Proof.assert_bottom true) state then ending int state
+ else raise Toplevel.UNDEF);
fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
--- a/src/Pure/Isar/locale.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/locale.ML Sat Jan 14 17:14:06 2006 +0100
@@ -475,7 +475,7 @@
if forall (equal "" o #1) ids then msg
else msg ^ "\n" ^ Pretty.string_of (Pretty.block
(Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
- in raise ProofContext.CONTEXT (err_msg, ctxt) end;
+ in error err_msg end;
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
@@ -668,7 +668,7 @@
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
| renaming (NONE :: xs) (y :: ys) = renaming xs ys
| renaming [] _ = []
- | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
+ | renaming xs [] = error ("Too many arguments in renaming: " ^
commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
fun rename_parms top ren ((name, ps), (parms, mode)) =
@@ -749,7 +749,7 @@
let
val (ids', parms', syn') = identify top e;
val ren = renaming xs parms'
- handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
+ handle ERROR msg => err_in_locale' ctxt msg ids';
val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
val parms'' = distinct (List.concat (map (#2 o #1) ids''));
@@ -869,7 +869,7 @@
val thy = ProofContext.theory_of ctxt;
val ((ctxt', _), res) =
foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
- handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
+ handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
val ctxt'' = if name = "" then ctxt'
else let
val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
@@ -992,8 +992,7 @@
(case elems of
Int es => foldl_map declare_int_elem (ctxt, es)
| Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
- handle ProofContext.CONTEXT (msg, ctxt) =>
- err_in_locale ctxt msg [(name, map fst ps)]
+ handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
in (ctxt', propps) end
| declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
@@ -1102,8 +1101,7 @@
in Term.list_all_free (frees, t) end;
fun no_binds [] = []
- | no_binds _ =
- raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
+ | no_binds _ = error "Illegal term bindings in locale element";
in
(case elem of
Assumes asms => Assumes (asms |> map (fn (a, propps) =>
@@ -1244,16 +1242,15 @@
local
-fun prep_name ctxt name =
- if NameSpace.is_qualified name then
- raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
+fun prep_name name =
+ if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
else name;
fun prep_facts _ _ ctxt (Int elem) =
Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
| prep_facts get intern ctxt (Ext elem) = elem |> Element.map_ctxt
{var = I, typ = I, term = I,
- name = prep_name ctxt,
+ name = prep_name,
fact = get ctxt,
attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
--- a/src/Pure/Isar/obtain.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/obtain.ML Sat Jan 14 17:14:06 2006 +0100
@@ -52,7 +52,7 @@
(** obtain_export **)
-fun obtain_export state parms rule cprops thm =
+fun obtain_export ctxt parms rule cprops thm =
let
val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
val cparms = map (Thm.cterm_of thy) parms;
@@ -67,10 +67,10 @@
val bads = parms inter (Term.term_frees concl);
in
if not (null bads) then
- raise Proof.STATE ("Conclusion contains obtained parameters: " ^
- space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
+ error ("Conclusion contains obtained parameters: " ^
+ space_implode " " (map (ProofContext.string_of_term ctxt) bads))
else if not (ObjectLogic.is_judgment thy concl) then
- raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state)
+ error "Conclusion in obtained context must be object-logic judgments"
else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
end;
@@ -92,6 +92,7 @@
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
+ val thy = Proof.theory_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
(*obtain vars*)
@@ -103,7 +104,7 @@
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
val asm_props = List.concat (map (map fst) proppss);
- val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss;
+ val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
@@ -129,7 +130,7 @@
Proof.local_qed (NONE, false)
#> Seq.map (`Proof.the_fact #-> (fn rule =>
Proof.fix_i (xs ~~ Ts)
- #> Proof.assm_i (K (obtain_export state parms rule)) asms));
+ #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
in
state
|> Proof.enter_forward
@@ -157,14 +158,13 @@
local
-fun match_params state vars rule =
+fun match_params ctxt vars rule =
let
- val ctxt = Proof.context_of state;
- val thy = Proof.theory_of state;
+ val thy = ProofContext.theory_of ctxt;
val string_of_typ = ProofContext.string_of_typ ctxt;
val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
- fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state);
+ fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
val m = length vars;
@@ -214,26 +214,23 @@
[prem] =>
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then ()
- else raise Proof.STATE ("Guessed a different clause:\n" ^
- ProofContext.string_of_thm ctxt th, state)
- | [] => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
- | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
- ProofContext.string_of_thm ctxt th, state));
+ else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
+ | [] => error "Goal solved -- nothing guessed."
+ | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
fun guess_context raw_rule =
let
- val (parms, rule) = match_params state (map (fn (x, T, _) => (x, T)) vars) raw_rule;
+ val (parms, rule) = match_params ctxt (map (fn (x, T, _) => (x, T)) vars) raw_rule;
val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
val ts = map (bind o Free) parms;
val ps = map dest_Free ts;
val asms =
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
|> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
- val _ = conditional (null asms) (fn () =>
- raise Proof.STATE ("Trivial result -- nothing guessed", state));
+ val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
in
Proof.fix_i (map (apsnd SOME) parms)
- #> Proof.assm_i (K (obtain_export state ts rule)) [(("", []), asms)]
+ #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
#> Proof.add_binds_i AutoBind.no_facts
end;
--- a/src/Pure/Isar/proof.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/proof.ML Sat Jan 14 17:14:06 2006 +0100
@@ -10,7 +10,6 @@
type context (*= Context.proof*)
type method (*= Method.method*)
type state
- exception STATE of string * state
val init: context -> state
val level: state -> int
val assert_bottom: bool -> state -> state
@@ -164,8 +163,6 @@
(thm list list -> state -> state Seq.seq) *
(thm list list -> theory -> theory)};
-exception STATE of string * state;
-
fun make_goal (statement, using, goal, before_qed, after_qed) =
Goal {statement = statement, using = using, goal = goal,
before_qed = before_qed, after_qed = after_qed};
@@ -189,15 +186,15 @@
fun open_block (State st) = State (Stack.push st);
-fun close_block (state as State st) = State (Stack.pop st)
- handle Empty => raise STATE ("Unbalanced block parentheses", state);
+fun close_block (State st) = State (Stack.pop st)
+ handle Empty => error "Unbalanced block parentheses";
fun level (State st) = Stack.level st;
fun assert_bottom b state =
let val b' = (level state <= 2) in
- if b andalso not b' then raise STATE ("Not at bottom of proof!", state)
- else if not b andalso b' then raise STATE ("Already at bottom of proof!", state)
+ if b andalso not b' then error "Not at bottom of proof!"
+ else if not b andalso b' then error "Already at bottom of proof!"
else state
end;
@@ -226,11 +223,11 @@
fun the_facts state =
(case get_facts state of SOME facts => facts
- | NONE => raise STATE ("No current facts available", state));
+ | NONE => error "No current facts available");
fun the_fact state =
(case the_facts state of [thm] => thm
- | _ => raise STATE ("Single theorem expected", state));
+ | _ => error "Single theorem expected");
fun put_facts facts =
map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
@@ -258,8 +255,7 @@
fun assert_mode pred state =
let val mode = get_mode state in
if pred mode then state
- else raise STATE ("Illegal application of proof command in "
- ^ quote (mode_name mode) ^ " mode", state)
+ else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
end;
val assert_forward = assert_mode (equal Forward);
@@ -278,12 +274,12 @@
fun current_goal state =
(case current state of
{context, goal = SOME (Goal goal), ...} => (context, goal)
- | _ => raise STATE ("No current goal!", state));
+ | _ => error "No current goal!");
fun assert_current_goal g state =
let val g' = can current_goal state in
- if g andalso not g' then raise STATE ("No goal in this block!", state)
- else if not g andalso g' then raise STATE ("Goal present in this block!", state)
+ if g andalso not g' then error "No goal in this block!"
+ else if not g andalso g' then error "Goal present in this block!"
else state
end;
@@ -311,8 +307,7 @@
fun find i state =
(case try current_goal state of
SOME (ctxt, goal) => (ctxt, (i, goal))
- | NONE => find (i + 1) (close_block state
- handle STATE _ => raise STATE ("No goal present", state)));
+ | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
in val find_goal = find 0 end;
fun get_goal state =
@@ -394,7 +389,7 @@
fun check_theory thy state =
if subthy (thy, theory_of state) then state
- else raise STATE ("Bad theory of method result: " ^ Context.str_of_thy thy, state);
+ else error ("Bad theory of method result: " ^ Context.str_of_thy thy);
fun apply_method current_context meth_fun state =
let
@@ -466,23 +461,22 @@
fun conclude_goal state goal propss =
let
val ctxt = context_of state;
- fun err msg = raise STATE (msg, state);
val ngoals = Thm.nprems_of goal;
val _ = conditional (ngoals > 0) (fn () =>
- err (Pretty.string_of (Pretty.chunks
+ error (Pretty.string_of (Pretty.chunks
(pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
val {hyps, thy, ...} = Thm.rep_thm goal;
val bad_hyps = fold (remove (op aconv)) (ProofContext.assms_of ctxt) hyps;
- val _ = conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
+ val _ = conditional (not (null bad_hyps)) (fn () => error ("Additional hypotheses:\n" ^
cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
val th = Goal.conclude goal;
val _ = conditional (not (Pattern.matches thy
(Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
- err ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
+ error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
in Drule.conj_elim_precise (map length propss) th end;
@@ -759,8 +753,8 @@
fun check_tvars props state =
(case fold Term.add_tvars props [] of [] => ()
- | tvars => raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
- commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars), state));
+ | tvars => error ("Goal statement contains illegal schematic type variable(s): " ^
+ commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars)));
fun check_vars props state =
(case fold Term.add_vars props [] of [] => ()
@@ -873,9 +867,9 @@
before_qed (K Seq.single, after_qed') propp
end;
-fun check_result msg state sq =
+fun check_result msg sq =
(case Seq.pull sq of
- NONE => raise STATE (msg, state)
+ NONE => error msg
| SOME res => Seq.cons res);
fun global_qeds txt =
@@ -886,11 +880,10 @@
|> Seq.map (rpair (context_of state)))
|> Seq.DETERM; (*backtracking may destroy theory!*)
-fun global_qed txt state =
- state
- |> global_qeds txt
- |> check_result "Failed to finish proof" state
- |> Seq.hd;
+fun global_qed txt =
+ global_qeds txt
+ #> check_result "Failed to finish proof"
+ #> Seq.hd;
(* concluding steps *)
@@ -903,13 +896,12 @@
val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
-fun global_term_proof immed (text, opt_text) state =
- state
- |> proof (SOME text)
- |> check_result "Terminal proof method failed" state
- |> Seq.maps (global_qeds (opt_text, immed))
- |> check_result "Failed to finish proof (after successful terminal method)" state
- |> Seq.hd;
+fun global_term_proof immed (text, opt_text) =
+ proof (SOME text)
+ #> check_result "Terminal proof method failed"
+ #> Seq.maps (global_qeds (opt_text, immed))
+ #> check_result "Failed to finish proof (after successful terminal method)"
+ #> Seq.hd;
val global_terminal_proof = global_term_proof true;
val global_default_proof = global_terminal_proof (Method.default_text, NONE);
@@ -944,7 +936,6 @@
(Seq.pull oo local_skip_proof) true
|> setmp testing true
|> setmp proofs 0
- |> transform_error
|> capture;
fun after_qed' results =
@@ -956,7 +947,7 @@
|> K int ? (fn goal_state =>
(case test_proof goal_state of
Result (SOME _) => goal_state
- | Result NONE => raise STATE (fail_msg (context_of goal_state), goal_state)
+ | Result NONE => error (fail_msg (context_of goal_state))
| Exn Interrupt => raise Interrupt
| Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))
end;
--- a/src/Pure/Isar/proof_context.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Jan 14 17:14:06 2006 +0100
@@ -11,7 +11,6 @@
sig
type context (*= Context.proof*)
type export
- exception CONTEXT of string * context
val theory_of: context -> theory
val init: theory -> context
val set_body: bool -> context -> context
@@ -161,7 +160,6 @@
struct
type context = Context.proof;
-exception CONTEXT = Context.PROOF;
val theory_of = Context.theory_of_proof;
val init = Context.init_proof;
@@ -289,10 +287,10 @@
local
-fun check_mixfix ctxt (x, _, mx) =
+fun check_mixfix (x, _, mx) =
if mx <> NoSyn andalso mx <> Structure andalso
(can Syntax.dest_internal x orelse can Syntax.dest_skolem x) then
- raise CONTEXT ("Illegal mixfix syntax for internal/skolem constant " ^ quote x, ctxt)
+ error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
else ();
fun mixfix x NONE mx = (Syntax.fixedN ^ x, TypeInfer.mixfixT mx, Syntax.fix_mixfix x mx)
@@ -329,7 +327,7 @@
val is_logtype = Sign.is_logtype thy;
val structs' = structs @ List.mapPartial prep_struct decls;
- val mxs = List.mapPartial (tap (check_mixfix ctxt) #> prep_mixfix) decls;
+ val mxs = List.mapPartial (tap check_mixfix #> prep_mixfix) decls;
val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
val extend =
@@ -408,11 +406,11 @@
fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1);
fun infer_type ctxt x =
- (case try (transform_error (fn () =>
+ (case try (fn () =>
Sign.infer_types (pp ctxt) (theory_of ctxt) (def_type ctxt false) (def_sort ctxt)
- (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT))) () of
+ (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of
SOME (Free (_, T), _) => T
- | _ => raise CONTEXT ("Failed to infer type of fixed variable " ^ quote x, ctxt));
+ | _ => error ("Failed to infer type of fixed variable " ^ quote x));
@@ -421,12 +419,10 @@
local
fun read_typ_aux read ctxt s =
- transform_error (read (syn_of ctxt) (theory_of ctxt, def_sort ctxt)) s
- handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
+ read (syn_of ctxt) (theory_of ctxt, def_sort ctxt) s;
fun cert_typ_aux cert ctxt raw_T =
- cert (theory_of ctxt) raw_T
- handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
+ cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
in
@@ -445,11 +441,11 @@
val lookup_skolem = AList.lookup (op =) o fixes_of;
fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
-fun no_skolem internal ctxt x =
+fun no_skolem internal x =
if can Syntax.dest_skolem x then
- raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
+ error ("Illegal reference to internal Skolem constant: " ^ quote x)
else if not internal andalso can Syntax.dest_internal x then
- raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt)
+ error ("Illegal reference to internal variable: " ^ quote x)
else x;
fun intern_skolem ctxt internal =
@@ -457,7 +453,7 @@
fun intern (t as Free (x, T)) =
if internal x then t
else
- (case lookup_skolem ctxt (no_skolem false ctxt x) of
+ (case lookup_skolem ctxt (no_skolem false x) of
SOME x' => Free (x', T)
| NONE => t)
| intern (t $ u) = intern t $ intern u
@@ -546,7 +542,7 @@
in norm u' handle SAME => u' end
| NONE =>
if schematic then raise SAME
- else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
+ else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi))
| norm (Abs (a, T, body)) = Abs (a, T, norm body)
| norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
| norm (f $ t) =
@@ -567,8 +563,8 @@
in next := i; u end
end;
-fun reject_dummies ctxt t = Term.no_dummy_patterns t
- handle TERM _ => raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
+fun reject_dummies t = Term.no_dummy_patterns t
+ handle TERM _ => error "Illegal dummy pattern(s) in term";
(* read terms *)
@@ -584,12 +580,11 @@
val sorts = append_env (def_sort ctxt) more_sorts;
val used = used_types ctxt @ more_used;
in
- (transform_error (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used)) s
- handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
- | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
+ (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used) s
+ handle TERM (msg, _) => error msg)
|> app (intern_skolem ctxt internal)
|> app (if pattern then I else norm_term ctxt schematic)
- |> app (if pattern then prepare_dummies else reject_dummies ctxt)
+ |> app (if pattern then prepare_dummies else reject_dummies)
end;
fun gen_read read app pattern schematic ctxt =
@@ -623,8 +618,8 @@
fun gen_cert cert pattern schematic ctxt t = t
|> (if pattern then I else norm_term ctxt schematic)
|> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
- handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt)
- | TERM (msg, _) => raise CONTEXT (msg, ctxt));
+ handle TYPE (msg, _, _) => error msg
+ | TERM (msg, _) => error msg);
val certify_term = #1 ooo Sign.certify_term;
val certify_prop = #1 ooo Sign.certify_prop;
@@ -824,7 +819,7 @@
fun simult_matches ctxt [] = []
| simult_matches ctxt pairs =
let
- fun fail () = raise CONTEXT ("Pattern match failed!", ctxt);
+ fun fail () = error "Pattern match failed!";
val maxidx = fold (fn (t1, t2) => fn i =>
Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
@@ -970,8 +965,7 @@
let
val thy = theory_of ctxt;
val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
- handle ERROR_MESSAGE msg =>
- raise CONTEXT (msg ^ "\nFailed to retrieve literal fact.", ctxt);
+ handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
in pick "" [th] end
| retrieve_thms from_thy pick ctxt xthmref =
let
@@ -994,7 +988,7 @@
(* valid_thms *)
fun valid_thms ctxt (name, ths) =
- (case try (transform_error (fn () => get_thms ctxt (Name name))) () of
+ (case try (fn () => get_thms ctxt (Name name)) () of
NONE => false
| SOME ths' => Thm.eq_thms (ths, ths'));
@@ -1078,13 +1072,13 @@
val x = Syntax.const_name raw_x raw_mx;
val mx = Syntax.fix_mixfix raw_x raw_mx;
val _ =
- if not legacy andalso not (Syntax.is_identifier (no_skolem internal ctxt x)) then
- raise CONTEXT ("Illegal variable name: " ^ quote x, ctxt)
+ if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then
+ error ("Illegal variable name: " ^ quote x)
else ();
fun cond_tvars T =
if internal then T
- else Type.no_tvars T handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
+ else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
val var = (x, opt_T, mx);
in (var, ctxt |> declare_var var) end);
@@ -1104,7 +1098,7 @@
local
fun no_dups _ [] = ()
- | no_dups ctxt dups = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote dups, ctxt);
+ | no_dups ctxt dups = error ("Duplicate variable(s): " ^ commas_quote dups);
fun gen_fixes prep raw_vars ctxt =
let
@@ -1227,8 +1221,8 @@
fun cert_def ctxt eq =
let
- fun err msg = raise CONTEXT (msg ^
- "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt);
+ fun err msg = cat_error msg
+ ("The error(s) above occurred in local definition: " ^ string_of_term ctxt eq);
val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq)
handle TERM _ => err "Not a meta-equality (==)";
val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
@@ -1282,11 +1276,11 @@
| add_case _ (name, NONE) cases = rem_case name cases
| add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases;
-fun prep_case ctxt name fxs c =
+fun prep_case name fxs c =
let
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
| replace [] ys = ys
- | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
+ | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
val RuleCases.Case {fixes, assumes, binds, cases} = c;
val fixes' = replace fxs fixes;
val binds' = map drop_schematic binds;
@@ -1294,7 +1288,7 @@
if null (fold (Term.add_tvarsT o snd) fixes []) andalso
null (fold (fold Term.add_vars o snd) assumes []) then
RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
- else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
+ else error ("Illegal schematic variable(s) in case " ^ quote name)
end;
fun fix (x, T) ctxt =
@@ -1323,8 +1317,8 @@
fun get_case ctxt name xs =
(case AList.lookup (op =) (cases_of ctxt) name of
- NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
- | SOME (c, _) => prep_case ctxt name xs c);
+ NONE => error ("Unknown case: " ^ quote name)
+ | SOME (c, _) => prep_case name xs c);
end;
--- a/src/Pure/Isar/proof_history.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Isar/proof_history.ML Sat Jan 14 17:14:06 2006 +0100
@@ -8,7 +8,6 @@
signature PROOF_HISTORY =
sig
type T
- exception FAIL of string
val position: T -> int
val init: int option -> Proof.state -> T
val is_initial: T -> bool
@@ -36,8 +35,6 @@
datatype T = ProofHistory of proof History.T;
-exception FAIL of string;
-
fun app f (ProofHistory x) = ProofHistory (f x);
fun hist_app f = app (History.apply f);
@@ -59,7 +56,7 @@
val back = hist_app (fn ((_, stq), nodes) =>
(case Seq.pull stq of
- NONE => raise FAIL "back: no alternatives"
+ NONE => error "back: no alternatives"
| SOME result => (result, nodes)));
@@ -67,7 +64,7 @@
fun applys f = hist_app (fn (node as (st, _), nodes) =>
(case Seq.pull (f st) of
- NONE => raise FAIL "empty result sequence -- proof command failed"
+ NONE => error "empty result sequence -- proof command failed"
| SOME results => (results, node :: nodes)));
fun apply f = applys (Seq.single o f);
--- a/src/Pure/Syntax/syn_ext.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Sat Jan 14 17:14:06 2006 +0100
@@ -179,8 +179,7 @@
datatype mfix = Mfix of string * typ * string * int list * int;
fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
- error ((if msg = "" then "" else msg ^ "\n") ^
- "in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
+ cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
(* typ_to_nonterm *)
@@ -284,7 +283,7 @@
| logify_types _ a = a;
- val raw_symbs = read_mixfix sy handle ERROR => err_in_mfix "" mfix;
+ val raw_symbs = read_mixfix sy handle ERROR msg => err_in_mfix msg mfix;
val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
val (const', typ', parse_rules) =
if not (exists is_index args) then (const, typ, [])
--- a/src/Pure/Syntax/syn_trans.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Sat Jan 14 17:14:06 2006 +0100
@@ -203,7 +203,7 @@
fun the_struct structs i =
if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)
- else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
+ else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
Lexicon.free (the_struct structs 1)
@@ -424,7 +424,7 @@
fun the_struct' structs s =
[(case Lexicon.read_nat s of
- SOME i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
+ SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
| NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
--- a/src/Pure/Syntax/syntax.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Jan 14 17:14:06 2006 +0100
@@ -447,8 +447,8 @@
(case read_asts thy is_logtype syn true root str of
[ast] => constify ast
| _ => error ("Syntactically ambiguous input: " ^ quote str))
- end handle ERROR =>
- error ("The error(s) above occurred in translation pattern " ^
+ end handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in translation pattern " ^
quote str);
--- a/src/Pure/Thy/thy_info.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Jan 14 17:14:06 2006 +0100
@@ -356,9 +356,10 @@
val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict
(name :: initiators);
- val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
- error (loader_msg "the error(s) above occurred while examining theory" [name] ^
- (if null initiators then "" else required_by "\n" initiators));
+ val (current, (new_deps, parents)) = current_deps ml strict dir name
+ handle ERROR msg => cat_error msg
+ (loader_msg "the error(s) above occurred while examining theory" [name] ^
+ (if null initiators then "" else required_by "\n" initiators));
val dir' = if_none (opt_path'' new_deps) dir;
val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
--- a/src/Pure/axclass.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/axclass.ML Sat Jan 14 17:14:06 2006 +0100
@@ -274,8 +274,8 @@
val (c1, c2) = prep_classrel thy raw_cc;
val txt = quote (Sign.string_of_classrel thy [c1, c2]);
val _ = message ("Proving class inclusion " ^ txt ^ " ...");
- val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
- error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
+ val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred while trying to prove " ^ txt);
in add_classrel_thms [th] thy end;
fun ext_inst_arity prep_arity raw_arity tac thy =
@@ -285,9 +285,8 @@
val _ = message ("Proving type arity " ^ txt ^ " ...");
val props = (mk_arities arity);
val ths = Goal.prove_multi thy [] [] props
- (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
- handle ERROR_MESSAGE msg =>
- error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
+ (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
+ cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt);
in add_arity_thms ths thy end;
in
--- a/src/Pure/context.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/context.ML Sat Jan 14 17:14:06 2006 +0100
@@ -66,7 +66,6 @@
val setup: unit -> (theory -> theory) list
(*proof context*)
type proof
- exception PROOF of string * proof
val theory_of_proof: proof -> theory
val transfer_proof: theory -> proof -> proof
val init_proof: theory -> proof
@@ -475,7 +474,7 @@
(* use ML text *)
-val ml_output = (writeln, error_msg);
+val ml_output = (writeln, Output.error_msg);
fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
@@ -505,15 +504,13 @@
datatype proof = Proof of theory_ref * Object.T Inttab.table;
-exception PROOF of string * proof;
-
fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
fun data_of_proof (Proof (_, data)) = data;
fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
if not (subthy (deref thy_ref, thy')) then
- raise PROOF ("transfer proof context: no a super theory", prf)
+ error "transfer proof context: no a super theory"
else Proof (self_ref thy', data);
--- a/src/Pure/goal.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/goal.ML Sat Jan 14 17:14:06 2006 +0100
@@ -123,8 +123,8 @@
val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
- fun err msg = raise ERROR_MESSAGE
- (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
+ fun err msg = cat_error msg
+ ("The error(s) above occurred for the goal statement:\n" ^
Sign.string_of_term thy (Term.list_all_free (params, statement)));
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
@@ -165,7 +165,7 @@
fun prove_raw casms cprop tac =
(case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
SOME th => Drule.implies_intr_list casms (finish th)
- | NONE => raise ERROR_MESSAGE "Tactic failed.");
+ | NONE => error "Tactic failed.");
(* SELECT_GOAL *)
--- a/src/Pure/old_goals.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/old_goals.ML Sat Jan 14 17:14:06 2006 +0100
@@ -220,7 +220,7 @@
| e => raise e;
(*Prints an exception, then fails*)
-fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR);
+fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR "");
(** the prove_goal.... commands
Prove theorem using the listed tactics; check it has the specified form.
@@ -252,7 +252,7 @@
fun prove_goalw thy rths agoal tacsf =
let val chorn = read_cterm thy (agoal, propT)
in prove_goalw_cterm_general true rths chorn tacsf end
- handle ERROR => error (*from read_cterm?*)
+ handle ERROR msg => cat_error msg (*from read_cterm?*)
("The error(s) above occurred for " ^ quote agoal);
(*String version with no meta-rewrite-rules*)
@@ -365,7 +365,7 @@
(*Version taking the goal as a string*)
fun agoalw atomic thy rths agoal =
agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
- handle ERROR => error (*from type_assign, etc via prepare_proof*)
+ handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
("The error(s) above occurred for " ^ quote agoal);
val goalw = agoalw false;
--- a/src/Pure/proof_general.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/proof_general.ML Sat Jan 14 17:14:06 2006 +0100
@@ -431,7 +431,7 @@
let val name = thy_name file in
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
(ThyInfo.touch_child_thys name;
- transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
+ ThyInfo.pretend_use_thy_only name handle ERROR msg =>
(warning msg; warning ("Failed to register theory: " ^ quote name);
tell_file_retracted (Path.base (Path.unpack file))))
else raise Toplevel.UNDEF
@@ -639,7 +639,7 @@
in
if exists then
(issue_pgips [proverinfo]; issue_pgips [File.read path])
- else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
+ else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
end;
end
@@ -1302,9 +1302,9 @@
else false
end)
| _ => raise PGIP "Invalid PGIP packet received")
- handle (PGIP msg) =>
- (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
- (XML.string_of_tree xml))))
+ handle PGIP msg =>
+ error (msg ^ "\nPGIP error occured in XML text below:\n" ^
+ (XML.string_of_tree xml)))
val process_pgip = K () o process_pgip_tree o XML.tree_of_string
@@ -1336,9 +1336,8 @@
and handler (e,srco) =
case (e,srco) of
(XML_PARSE,SOME src) =>
- panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
+ Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
| (PGIP_QUIT,_) => ()
- | (ERROR,SOME src) => loop true src (* message already given *)
| (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
| (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
| (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
@@ -1441,7 +1440,7 @@
(init_setup isar false;
if isar then Isar.sync_main () else isa_restart ());
-fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode."
+fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
| init_pgip true = (init_setup true true; pgip_toplevel tty_src);
--- a/src/Pure/pure_thy.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/pure_thy.ML Sat Jan 14 17:14:06 2006 +0100
@@ -176,7 +176,7 @@
fun name_of_thmref (Name name) = name
| name_of_thmref (NameSelection (name, _)) = name
- | name_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
+ | name_of_thmref (Fact _) = error "Illegal literal fact";
fun map_name_of_thmref f (Name name) = Name (f name)
| map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
@@ -185,7 +185,7 @@
fun string_of_thmref (Name name) = name
| string_of_thmref (NameSelection (name, is)) =
name ^ enclose "(" ")" (commas (map string_of_interval is))
- | string_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
+ | string_of_thmref (Fact _) = error "Illegal literal fact";
(* select_thm *)
@@ -254,7 +254,7 @@
(* thms_containing etc. *)
fun valid_thms thy (thmref, ths) =
- (case try (transform_error (get_thms thy)) thmref of
+ (case try (get_thms thy) thmref of
NONE => false
| SOME ths' => Thm.eq_thms (ths, ths'));
--- a/src/Pure/sign.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/sign.ML Sat Jan 14 17:14:06 2006 +0100
@@ -477,7 +477,7 @@
val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
in cert thy T handle TYPE (msg, _, _) => error msg end
- handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
+ handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
fun gen_read_typ cert (thy, def_sort) str =
gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
@@ -531,31 +531,29 @@
val typs =
map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
- fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
+ fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
(const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
(intern_sort thy) used freeze typs ts)
- handle TYPE (msg, _, _) => Error msg;
+ handle TYPE (msg, _, _) => Exn (ERROR msg);
val err_results = map infer termss;
- val errs = List.mapPartial get_error err_results;
- val results = List.mapPartial get_ok err_results;
+ val errs = List.mapPartial (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
+ val results = List.mapPartial get_result err_results;
val ambiguity = length termss;
-
fun ambig_msg () =
- if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level
- then
- error_msg "Got more than one parse tree.\n\
- \Retry with smaller Syntax.ambiguity_level for more information."
- else ();
+ if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then
+ "Got more than one parse tree.\n\
+ \Retry with smaller Syntax.ambiguity_level for more information."
+ else "";
in
- if null results then (ambig_msg (); error (cat_lines errs))
+ if null results then (cat_error (ambig_msg ()) (cat_lines errs))
else if length results = 1 then
(if ambiguity > ! Syntax.ambiguity_level then
warning "Fortunately, only one parse tree is type correct.\n\
\You may still want to disambiguate your grammar or your input."
else (); hd results)
- else (ambig_msg (); error ("More than one term is type correct:\n" ^
+ else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
end;
@@ -578,7 +576,7 @@
fun simple_read_term thy T s =
let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
in t end
- handle ERROR => error ("The error(s) above occurred for term " ^ s);
+ handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
fun read_term thy = simple_read_term thy TypeInfer.logicT;
fun read_prop thy = simple_read_term thy propT;
@@ -630,7 +628,7 @@
val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
val a' = Syntax.type_name a mx;
val abbr = (a', vs, prep_typ thy rhs)
- handle ERROR => error ("in type abbreviation " ^ quote a');
+ handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
val tsig' = Type.add_abbrevs naming [abbr] tsig;
in (naming, syn', tsig', consts) end);
@@ -643,7 +641,7 @@
fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
let
fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
- handle ERROR => error ("in arity for type " ^ quote a);
+ handle ERROR msg => cat_error msg ("in arity for type " ^ quote a);
val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
in tsig' end);
@@ -655,8 +653,8 @@
fun gen_syntax change_gram prep_typ prmode args thy =
let
- fun prep (c, T, mx) = (c, prep_typ thy T, mx)
- handle ERROR => error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
+ fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
+ cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
in thy |> map_syn (change_gram (is_logtype thy) prmode (map prep args)) end;
fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
@@ -677,7 +675,8 @@
let
val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
- handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
+ handle ERROR msg =>
+ cat_error msg ("in declaration of constant " ^ quote (Syntax.const_name c mx));
val args = map prep raw_args;
val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, T));
in
--- a/src/Pure/theory.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/theory.ML Sat Jan 14 17:14:06 2006 +0100
@@ -163,8 +163,8 @@
(* prepare axioms *)
-fun err_in_axm name =
- error ("The error(s) above occurred in axiom " ^ quote name);
+fun err_in_axm msg name =
+ cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
fun no_vars pp tm =
(case (Term.term_vars tm, Term.term_tvars tm) of
@@ -190,7 +190,7 @@
val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
in cert_axm thy (name, t) end
- handle ERROR => err_in_axm name;
+ handle ERROR msg => err_in_axm msg name;
fun read_axm thy name_str = read_def_axm (thy, K NONE, K NONE) [] name_str;
@@ -199,7 +199,7 @@
val pp = Sign.pp thy;
val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
in (name, no_vars pp t) end
- handle ERROR => err_in_axm name;
+ handle ERROR msg => err_in_axm msg name;
(* add_axioms(_i) *)
@@ -309,7 +309,7 @@
defs |> Defs.define (Sign.the_const_type thy)
name (prep_const thy const) (map (prep_const thy) rhs_consts)
end
- handle ERROR => error (Pretty.string_of (Pretty.block
+ handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
[Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
--- a/src/Sequents/LK/quant.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Sequents/LK/quant.ML Sat Jan 14 17:14:06 2006 +0100
@@ -97,22 +97,22 @@
(*INVALID*)
goal (theory "LK") "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
(*INVALID*)
goal (theory "LK") "|- (EX x. Q(x)) --> (ALL x. Q(x))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;
--- a/src/ZF/Datatype.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/ZF/Datatype.ML Sat Jan 14 17:14:06 2006 +0100
@@ -89,7 +89,7 @@
val goal = Logic.mk_equals (old, new)
val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
- handle ERROR_MESSAGE msg =>
+ handle ERROR msg =>
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
raise Match)
in SOME thm end
--- a/src/ZF/Tools/ind_cases.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML Sat Jan 14 17:14:06 2006 +0100
@@ -35,10 +35,10 @@
fun smart_cases thy ss read_prop s =
let
- fun err () = error ("Malformed set membership statement: " ^ s);
- val A = read_prop s handle ERROR => err ();
+ fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
+ val A = read_prop s handle ERROR msg => err msg;
val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
- (Logic.strip_imp_concl A)))))) handle TERM _ => err ();
+ (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
in
(case Symtab.lookup (IndCasesData.get thy) c of
NONE => error ("Unknown inductive cases rule for set " ^ quote c)
--- a/src/ZF/arith_data.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/ZF/arith_data.ML Sat Jan 14 17:14:06 2006 +0100
@@ -75,7 +75,7 @@
val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
- handle ERROR_MESSAGE msg =>
+ handle ERROR msg =>
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
end;