# HG changeset patch # User wenzelm # Date 1137255246 -3600 # Node ID dd0c569fa43d641dfe822fd79fd1d8c99d157c95 # Parent 01265301db7f013a38a5e7cb64e4f9f0e6495dcf sane ERROR handling; diff -r 01265301db7f -r dd0c569fa43d TFL/casesplit.ML --- 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 = diff -r 01265301db7f -r dd0c569fa43d TFL/post.ML --- 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 = diff -r 01265301db7f -r dd0c569fa43d TFL/rules.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d TFL/tfl.ML --- 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, diff -r 01265301db7f -r dd0c569fa43d src/CTT/ex/elim.ML --- 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"; diff -r 01265301db7f -r dd0c569fa43d src/FOL/ex/IffOracle.thy --- 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" *} diff -r 01265301db7f -r dd0c569fa43d src/FOL/ex/foundn.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/FOL/ex/int.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/FOL/ex/quant.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/FOLP/ex/foundn.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/FOLP/ex/int.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/FOLP/ex/quant.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/HOL/Import/proof_kernel.ML --- 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:" diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/datatype_package.ML --- 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') = diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/inductive_package.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/primrec_package.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/record_package.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/refute.ML --- 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 *) diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/sat_solver.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/HOL/Tools/typedef_package.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/HOL/ex/ROOT.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/HOLCF/adm_tac.ML --- 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) ***) diff -r 01265301db7f -r dd0c569fa43d src/HOLCF/cont_consts.ML --- 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)); diff -r 01265301db7f -r dd0c569fa43d src/HOLCF/domain/theorems.ML --- 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 ------------------------------------- *) diff -r 01265301db7f -r dd0c569fa43d src/HOLCF/pcpodef_package.ML --- 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 *) diff -r 01265301db7f -r dd0c569fa43d src/Provers/induct_method.ML --- 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))])) diff -r 01265301db7f -r dd0c569fa43d src/Pure/General/file.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/IsaPlanner/isand.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/attrib.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/calculation.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/isar_output.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/isar_thy.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/locale.ML --- 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)}; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/obtain.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/proof.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/proof_context.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/Isar/proof_history.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/Syntax/syn_ext.ML --- 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, []) diff -r 01265301db7f -r dd0c569fa43d src/Pure/Syntax/syn_trans.ML --- 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"] = diff -r 01265301db7f -r dd0c569fa43d src/Pure/Syntax/syntax.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/Thy/thy_info.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/axclass.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/Pure/context.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/goal.ML --- 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 *) diff -r 01265301db7f -r dd0c569fa43d src/Pure/old_goals.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/Pure/proof_general.ML --- 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); diff -r 01265301db7f -r dd0c569fa43d src/Pure/pure_thy.ML --- 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')); diff -r 01265301db7f -r dd0c569fa43d src/Pure/sign.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/Pure/theory.ML --- 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)])); diff -r 01265301db7f -r dd0c569fa43d src/Sequents/LK/quant.ML --- 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; diff -r 01265301db7f -r dd0c569fa43d src/ZF/Datatype.ML --- 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 diff -r 01265301db7f -r dd0c569fa43d src/ZF/Tools/ind_cases.ML --- 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) diff -r 01265301db7f -r dd0c569fa43d src/ZF/arith_data.ML --- 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;