prefer explicitly qualified exceptions, which is particular important for robust handlers;
authorwenzelm
Sat May 11 16:57:18 2013 +0200 (2013-05-11)
changeset 5193052fd62618631
parent 51929 5e8a0b8bb070
child 51931 7c517c92d315
prefer explicitly qualified exceptions, which is particular important for robust handlers;
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/Matrix_LP/Cplex_tools.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/groebner.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/basics.ML
src/Pure/type.ML
src/Tools/Code/code_namespace.ML
src/Tools/WWW_Find/http_util.ML
src/Tools/WWW_Find/socket_util.ML
src/ZF/Datatype_ZF.thy
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:13:08 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:57:18 2013 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4    {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
     1.5     bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
     1.6  
     1.7 -fun dest_cons [] = raise Empty
     1.8 +fun dest_cons [] = raise List.Empty
     1.9    | dest_cons (x :: xs) = (x, xs);
    1.10  
    1.11  fun mk_axioms n thms = thms
     2.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:13:08 2013 +0200
     2.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:57:18 2013 +0200
     2.3 @@ -973,7 +973,7 @@
     2.4      result
     2.5      end
     2.6      handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
     2.7 -     | Option => raise (Load_cplexResult "Option")
     2.8 +     | Option.Option => raise (Load_cplexResult "Option")
     2.9  
    2.10  fun load_cplexResult name =
    2.11      let
    2.12 @@ -1122,7 +1122,7 @@
    2.13      result
    2.14      end
    2.15      handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
    2.16 -     | Option => raise (Load_cplexResult "Option")
    2.17 +     | Option.Option => raise (Load_cplexResult "Option")
    2.18  
    2.19  exception Execute of string;
    2.20  
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 11 16:13:08 2013 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 11 16:57:18 2013 +0200
     3.3 @@ -194,7 +194,7 @@
     3.4               [s] => the_default (s, s) (first_field "\<emdash>" s)
     3.5             | ["", s2] => ("-" ^ s2, "-" ^ s2)
     3.6             | [s1, s2] => (s1, s2)
     3.7 -           | _ => raise Option)
     3.8 +           | _ => raise Option.Option)
     3.9            |> pairself (maxed_int_from_string min_int)
    3.10        in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
    3.11        handle Option.Option =>
     4.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat May 11 16:13:08 2013 +0200
     4.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 11 16:57:18 2013 +0200
     4.3 @@ -384,9 +384,9 @@
     4.4            (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
     4.5      in
     4.6        fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
     4.7 -        handle Option =>
     4.8 +        handle Option.Option =>
     4.9            (writeln ("noz: Theorems-Table contains no entry for " ^
    4.10 -              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
    4.11 +              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option)
    4.12      end
    4.13    fun unit_conv t =
    4.14     case (term_of t) of
    4.15 @@ -472,9 +472,9 @@
    4.16   val dvd =
    4.17     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
    4.18       fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
    4.19 -       handle Option =>
    4.20 +       handle Option.Option =>
    4.21          (writeln ("dvd: Theorems-Table contains no entry for" ^
    4.22 -            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
    4.23 +            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option)
    4.24     end
    4.25   val dp =
    4.26     let val th = Simplifier.rewrite (put_simpset lin_ss ctxt)
    4.27 @@ -541,9 +541,9 @@
    4.28                    sths) Termtab.empty
    4.29          in
    4.30            fn ct => the (Termtab.lookup tab (term_of ct))
    4.31 -            handle Option =>
    4.32 +            handle Option.Option =>
    4.33                (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
    4.34 -                raise Option)
    4.35 +                raise Option.Option)
    4.36          end
    4.37         val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
    4.38     in [dp, inf, nb, pd] MRS cpth
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 16:13:08 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 16:57:18 2013 +0200
     5.3 @@ -41,9 +41,9 @@
     5.4  fun pop tab key =
     5.5    (let val v = hd (Inttab.lookup_list tab key) in
     5.6      (v, Inttab.remove_list (op =) (key, v) tab)
     5.7 -  end) handle Empty => raise Fail "sledgehammer_compress: pop"
     5.8 +  end) handle List.Empty => raise Fail "sledgehammer_compress: pop"
     5.9  fun pop_max tab = pop tab (the (Inttab.max_key tab))
    5.10 -  handle Option => raise Fail "sledgehammer_compress: pop_max"
    5.11 +  handle Option.Option => raise Fail "sledgehammer_compress: pop_max"
    5.12  fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    5.13  
    5.14  (* Main function for compresing proofs *)
    5.15 @@ -104,7 +104,7 @@
    5.16            | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
    5.17                cons (Term.size_of_term t, i)
    5.18            | _ => I)
    5.19 -            handle Option => raise Fail "sledgehammer_compress: add_if_cand")
    5.20 +            handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand")
    5.21          | add_if_cand _ _ = I
    5.22        val cand_tab =
    5.23          v_fold_index (add_if_cand step_vect) refed_by_vect []
    5.24 @@ -121,7 +121,7 @@
    5.25               #> handle_metis_fail
    5.26               #> Lazy.lazy)
    5.27            step_vect
    5.28 -        handle Option => raise Fail "sledgehammer_compress: metis_time"
    5.29 +        handle Option.Option => raise Fail "sledgehammer_compress: metis_time"
    5.30  
    5.31        fun sum_up_time lazy_time_vector =
    5.32          Vector.foldl
    5.33 @@ -204,7 +204,7 @@
    5.34                            (n_metis' - 1)
    5.35              end
    5.36            end
    5.37 -        handle Option => raise Fail "sledgehammer_compress: merge_steps"
    5.38 +        handle Option.Option => raise Fail "sledgehammer_compress: merge_steps"
    5.39               | List.Empty => raise Fail "sledgehammer_compress: merge_steps"
    5.40      in
    5.41        merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat May 11 16:13:08 2013 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat May 11 16:57:18 2013 +0200
     6.3 @@ -58,11 +58,11 @@
     6.4  
     6.5  fun parse_bool_option option name s =
     6.6    (case s of
     6.7 -     "smart" => if option then NONE else raise Option
     6.8 +     "smart" => if option then NONE else raise Option.Option
     6.9     | "false" => SOME false
    6.10     | "true" => SOME true
    6.11     | "" => SOME true
    6.12 -   | _ => raise Option)
    6.13 +   | _ => raise Option.Option)
    6.14    handle Option.Option =>
    6.15           let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
    6.16             error ("Parameter " ^ quote name ^ " must be assigned " ^
     7.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sat May 11 16:13:08 2013 +0200
     7.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 11 16:57:18 2013 +0200
     7.3 @@ -604,7 +604,7 @@
     7.4        val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
     7.5        val plist = ListPair.zip (vlist, xlist)
     7.6        val args = map (the o AList.lookup (op aconv) plist) qvars
     7.7 -                   handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
     7.8 +                   handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
     7.9        fun build ex      []   = []
    7.10          | build (_$rex) (v::rst) =
    7.11             let val ex1 = Term.betapply(rex, v)
     8.1 --- a/src/HOL/Tools/groebner.ML	Sat May 11 16:13:08 2013 +0200
     8.2 +++ b/src/HOL/Tools/groebner.ML	Sat May 11 16:57:18 2013 +0200
     8.3 @@ -864,7 +864,7 @@
     8.4    val (vars,bod) = strip_exists tm
     8.5    val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
     8.6    val th1 = (the (get_first (try (isolate_variable vars)) cjs)
     8.7 -             handle Option => raise CTERM ("unwind_polys_conv",[tm]))
     8.8 +             handle Option.Option => raise CTERM ("unwind_polys_conv",[tm]))
     8.9    val eq = Thm.lhs_of th1
    8.10    val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
    8.11    val th2 = conj_ac_rule (mk_eq bod bod')
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat May 11 16:13:08 2013 +0200
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat May 11 16:57:18 2013 +0200
     9.3 @@ -498,7 +498,7 @@
     9.4            (case try_add ([thm1] RL inj_thms) thm2 of
     9.5              NONE =>
     9.6                (the (try_add ([thm2] RL inj_thms) thm1)
     9.7 -                handle Option =>
     9.8 +                handle Option.Option =>
     9.9                    (trace_thm ctxt [] thm1; trace_thm ctxt [] thm2;
    9.10                     raise Fail "Linear arithmetic: failed to add thms"))
    9.11            | SOME thm => thm)
    10.1 --- a/src/Pure/General/basics.ML	Sat May 11 16:13:08 2013 +0200
    10.2 +++ b/src/Pure/General/basics.ML	Sat May 11 16:57:18 2013 +0200
    10.3 @@ -78,7 +78,7 @@
    10.4    | is_none NONE = true;
    10.5  
    10.6  fun the (SOME x) = x
    10.7 -  | the NONE = raise Option;
    10.8 +  | the NONE = raise Option.Option;
    10.9  
   10.10  fun these (SOME x) = x
   10.11    | these NONE = [];
    11.1 --- a/src/Pure/type.ML	Sat May 11 16:13:08 2013 +0200
    11.2 +++ b/src/Pure/type.ML	Sat May 11 16:57:18 2013 +0200
    11.3 @@ -379,11 +379,11 @@
    11.4  
    11.5  fun freeze_one alist (ix, sort) =
    11.6    TFree (the (AList.lookup (op =) alist ix), sort)
    11.7 -    handle Option =>
    11.8 +    handle Option.Option =>
    11.9        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   11.10  
   11.11  fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
   11.12 -  handle Option => TFree (a, sort);
   11.13 +  handle Option.Option => TFree (a, sort);
   11.14  
   11.15  in
   11.16  
    12.1 --- a/src/Tools/Code/code_namespace.ML	Sat May 11 16:13:08 2013 +0200
    12.2 +++ b/src/Tools/Code/code_namespace.ML	Sat May 11 16:57:18 2013 +0200
    12.3 @@ -125,7 +125,7 @@
    12.4            Long_Name.append (fst (dest_name name)) (base_deresolver name)
    12.5        | deresolver module_name name =
    12.6            the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
    12.7 -          handle Option => error ("Unknown statement name: " ^ labelled_name name);
    12.8 +          handle Option.Option => error ("Unknown statement name: " ^ labelled_name name);
    12.9  
   12.10    in { deresolver = deresolver, flat_program = flat_program } end;
   12.11  
    13.1 --- a/src/Tools/WWW_Find/http_util.ML	Sat May 11 16:13:08 2013 +0200
    13.2 +++ b/src/Tools/WWW_Find/http_util.ML	Sat May 11 16:57:18 2013 +0200
    13.3 @@ -46,7 +46,7 @@
    13.4        |> Char.chr
    13.5        |> String.str
    13.6        |> Substring.full
    13.7 -      handle Option => c;
    13.8 +      handle Option.Option => c;
    13.9  
   13.10      fun f (done, s) =
   13.11        let
    14.1 --- a/src/Tools/WWW_Find/socket_util.ML	Sat May 11 16:13:08 2013 +0200
    14.2 +++ b/src/Tools/WWW_Find/socket_util.ML	Sat May 11 16:57:18 2013 +0200
    14.3 @@ -26,7 +26,7 @@
    14.4             |> NetHostDB.addr
    14.5             |> rpair port
    14.6             |> INetSock.toAddr
    14.7 -           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
    14.8 +           handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host));
    14.9      val _ = Socket.bind (sock, addr);
   14.10      val _ = Socket.listen (sock, 5);
   14.11    in sock end;
    15.1 --- a/src/ZF/Datatype_ZF.thy	Sat May 11 16:13:08 2013 +0200
    15.2 +++ b/src/ZF/Datatype_ZF.thy	Sat May 11 16:57:18 2013 +0200
    15.3 @@ -81,9 +81,9 @@
    15.4         val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
    15.5         val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
    15.6         val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
    15.7 -         handle Option => raise Match;
    15.8 +         handle Option.Option => raise Match;
    15.9         val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
   15.10 -         handle Option => raise Match;
   15.11 +         handle Option.Option => raise Match;
   15.12         val new =
   15.13             if #big_rec_name lcon_info = #big_rec_name rcon_info
   15.14                 andalso not (null (#free_iffs lcon_info)) then
    16.1 --- a/src/ZF/Tools/primrec_package.ML	Sat May 11 16:13:08 2013 +0200
    16.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat May 11 16:57:18 2013 +0200
    16.3 @@ -49,7 +49,7 @@
    16.4      val (cname, _) = dest_Const constr
    16.5        handle TERM _ => raise RecError "ill-formed constructor";
    16.6      val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
    16.7 -      handle Option =>
    16.8 +      handle Option.Option =>
    16.9        raise RecError "cannot determine datatype associated with function"
   16.10  
   16.11      val (ls, cargs, rs) = (map dest_Free ls_frees,