# HG changeset patch # User wenzelm # Date 1368284238 -7200 # Node ID 52fd62618631b24361ae340646a1afce699b90d4 # Parent 5e8a0b8bb070c64155ad7340421bfbb4c6c72b76 prefer explicitly qualified exceptions, which is particular important for robust handlers; diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Sat May 11 16:57:18 2013 +0200 @@ -123,7 +123,7 @@ {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel}; -fun dest_cons [] = raise Empty +fun dest_cons [] = raise List.Empty | dest_cons (x :: xs) = (x, xs); fun mk_axioms n thms = thms diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Matrix_LP/Cplex_tools.ML --- a/src/HOL/Matrix_LP/Cplex_tools.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML Sat May 11 16:57:18 2013 +0200 @@ -973,7 +973,7 @@ result end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) - | Option => raise (Load_cplexResult "Option") + | Option.Option => raise (Load_cplexResult "Option") fun load_cplexResult name = let @@ -1122,7 +1122,7 @@ result end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) - | Option => raise (Load_cplexResult "Option") + | Option.Option => raise (Load_cplexResult "Option") exception Execute of string; diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat May 11 16:57:18 2013 +0200 @@ -194,7 +194,7 @@ [s] => the_default (s, s) (first_field "\" s) | ["", s2] => ("-" ^ s2, "-" ^ s2) | [s1, s2] => (s1, s2) - | _ => raise Option) + | _ => raise Option.Option) |> pairself (maxed_int_from_string min_int) in if k1 <= k2 then k1 upto k2 else k1 downto k2 end handle Option.Option => diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat May 11 16:57:18 2013 +0200 @@ -384,9 +384,9 @@ (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number)) - handle Option => + handle Option.Option => (writeln ("noz: Theorems-Table contains no entry for " ^ - Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) + Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end fun unit_conv t = case (term_of t) of @@ -472,9 +472,9 @@ val dvd = let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (term_of ct |> dest_number)) - handle Option => + handle Option.Option => (writeln ("dvd: Theorems-Table contains no entry for" ^ - Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) + Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end val dp = let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) @@ -541,9 +541,9 @@ sths) Termtab.empty in fn ct => the (Termtab.lookup tab (term_of ct)) - handle Option => + handle Option.Option => (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); - raise Option) + raise Option.Option) end val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p in [dp, inf, nb, pd] MRS cpth diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat May 11 16:57:18 2013 +0200 @@ -41,9 +41,9 @@ fun pop tab key = (let val v = hd (Inttab.lookup_list tab key) in (v, Inttab.remove_list (op =) (key, v) tab) - end) handle Empty => raise Fail "sledgehammer_compress: pop" + end) handle List.Empty => raise Fail "sledgehammer_compress: pop" fun pop_max tab = pop tab (the (Inttab.max_key tab)) - handle Option => raise Fail "sledgehammer_compress: pop_max" + handle Option.Option => raise Fail "sledgehammer_compress: pop_max" fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab (* Main function for compresing proofs *) @@ -104,7 +104,7 @@ | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => cons (Term.size_of_term t, i) | _ => I) - handle Option => raise Fail "sledgehammer_compress: add_if_cand") + handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand") | add_if_cand _ _ = I val cand_tab = v_fold_index (add_if_cand step_vect) refed_by_vect [] @@ -121,7 +121,7 @@ #> handle_metis_fail #> Lazy.lazy) step_vect - handle Option => raise Fail "sledgehammer_compress: metis_time" + handle Option.Option => raise Fail "sledgehammer_compress: metis_time" fun sum_up_time lazy_time_vector = Vector.foldl @@ -204,7 +204,7 @@ (n_metis' - 1) end end - handle Option => raise Fail "sledgehammer_compress: merge_steps" + handle Option.Option => raise Fail "sledgehammer_compress: merge_steps" | List.Empty => raise Fail "sledgehammer_compress: merge_steps" in merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 16:57:18 2013 +0200 @@ -58,11 +58,11 @@ fun parse_bool_option option name s = (case s of - "smart" => if option then NONE else raise Option + "smart" => if option then NONE else raise Option.Option | "false" => SOME false | "true" => SOME true | "" => SOME true - | _ => raise Option) + | _ => raise Option.Option) handle Option.Option => let val ss = map quote ((option ? cons "smart") ["true", "false"]) in error ("Parameter " ^ quote name ^ " must be assigned " ^ diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Sat May 11 16:57:18 2013 +0200 @@ -604,7 +604,7 @@ val vlist = #2 (USyntax.strip_comb (USyntax.rhs body)) val plist = ListPair.zip (vlist, xlist) val args = map (the o AList.lookup (op aconv) plist) qvars - handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence" + handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence" fun build ex [] = [] | build (_$rex) (v::rst) = let val ex1 = Term.betapply(rex, v) diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/HOL/Tools/groebner.ML Sat May 11 16:57:18 2013 +0200 @@ -864,7 +864,7 @@ val (vars,bod) = strip_exists tm val cjs = striplist (dest_binary @{cterm HOL.conj}) bod val th1 = (the (get_first (try (isolate_variable vars)) cjs) - handle Option => raise CTERM ("unwind_polys_conv",[tm])) + handle Option.Option => raise CTERM ("unwind_polys_conv",[tm])) val eq = Thm.lhs_of th1 val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs)) val th2 = conj_ac_rule (mk_eq bod bod') diff -r 5e8a0b8bb070 -r 52fd62618631 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat May 11 16:57:18 2013 +0200 @@ -498,7 +498,7 @@ (case try_add ([thm1] RL inj_thms) thm2 of NONE => (the (try_add ([thm2] RL inj_thms) thm1) - handle Option => + handle Option.Option => (trace_thm ctxt [] thm1; trace_thm ctxt [] thm2; raise Fail "Linear arithmetic: failed to add thms")) | SOME thm => thm) diff -r 5e8a0b8bb070 -r 52fd62618631 src/Pure/General/basics.ML --- a/src/Pure/General/basics.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Pure/General/basics.ML Sat May 11 16:57:18 2013 +0200 @@ -78,7 +78,7 @@ | is_none NONE = true; fun the (SOME x) = x - | the NONE = raise Option; + | the NONE = raise Option.Option; fun these (SOME x) = x | these NONE = []; diff -r 5e8a0b8bb070 -r 52fd62618631 src/Pure/type.ML --- a/src/Pure/type.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Pure/type.ML Sat May 11 16:57:18 2013 +0200 @@ -379,11 +379,11 @@ fun freeze_one alist (ix, sort) = TFree (the (AList.lookup (op =) alist ix), sort) - handle Option => + handle Option.Option => raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []); fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort) - handle Option => TFree (a, sort); + handle Option.Option => TFree (a, sort); in diff -r 5e8a0b8bb070 -r 52fd62618631 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Tools/Code/code_namespace.ML Sat May 11 16:57:18 2013 +0200 @@ -125,7 +125,7 @@ Long_Name.append (fst (dest_name name)) (base_deresolver name) | deresolver module_name name = the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name) - handle Option => error ("Unknown statement name: " ^ labelled_name name); + handle Option.Option => error ("Unknown statement name: " ^ labelled_name name); in { deresolver = deresolver, flat_program = flat_program } end; diff -r 5e8a0b8bb070 -r 52fd62618631 src/Tools/WWW_Find/http_util.ML --- a/src/Tools/WWW_Find/http_util.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Tools/WWW_Find/http_util.ML Sat May 11 16:57:18 2013 +0200 @@ -46,7 +46,7 @@ |> Char.chr |> String.str |> Substring.full - handle Option => c; + handle Option.Option => c; fun f (done, s) = let diff -r 5e8a0b8bb070 -r 52fd62618631 src/Tools/WWW_Find/socket_util.ML --- a/src/Tools/WWW_Find/socket_util.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/Tools/WWW_Find/socket_util.ML Sat May 11 16:57:18 2013 +0200 @@ -26,7 +26,7 @@ |> NetHostDB.addr |> rpair port |> INetSock.toAddr - handle Option => raise Fail ("Cannot resolve hostname: " ^ host)); + handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host)); val _ = Socket.bind (sock, addr); val _ = Socket.listen (sock, 5); in sock end; diff -r 5e8a0b8bb070 -r 52fd62618631 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Sat May 11 16:13:08 2013 +0200 +++ b/src/ZF/Datatype_ZF.thy Sat May 11 16:57:18 2013 +0200 @@ -81,9 +81,9 @@ val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) - handle Option => raise Match; + handle Option.Option => raise Match; val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) - handle Option => raise Match; + handle Option.Option => raise Match; val new = if #big_rec_name lcon_info = #big_rec_name rcon_info andalso not (null (#free_iffs lcon_info)) then diff -r 5e8a0b8bb070 -r 52fd62618631 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sat May 11 16:13:08 2013 +0200 +++ b/src/ZF/Tools/primrec_package.ML Sat May 11 16:57:18 2013 +0200 @@ -49,7 +49,7 @@ val (cname, _) = dest_Const constr handle TERM _ => raise RecError "ill-formed constructor"; val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) - handle Option => + handle Option.Option => raise RecError "cannot determine datatype associated with function" val (ls, cargs, rs) = (map dest_Free ls_frees,