avoid excessive exceptions;
authorwenzelm
Wed Jul 13 16:07:33 2005 +0200 (2005-07-13)
changeset 1681123b9c52612db
parent 16810 2406588f99cb
child 16812 c7d38e714768
avoid excessive exceptions;
src/Pure/General/ord_list.ML
     1.1 --- a/src/Pure/General/ord_list.ML	Wed Jul 13 16:07:32 2005 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Wed Jul 13 16:07:33 2005 +0200
     1.3 @@ -24,32 +24,31 @@
     1.4  
     1.5  (* single elements *)
     1.6  
     1.7 -exception ABSENT of int;
     1.8 -
     1.9  fun find_index ord list x =
    1.10    let
    1.11 -    fun find i [] = raise ABSENT i
    1.12 +    fun find i [] = ~ i
    1.13        | find i (y :: ys) =
    1.14            (case ord (x, y) of
    1.15 -            LESS => raise ABSENT i
    1.16 +            LESS => ~ i
    1.17            | EQUAL => i
    1.18            | GREATER => find (i + 1) ys);
    1.19 -  in find 0 list end;
    1.20 +  in find 1 list end;
    1.21  
    1.22 -fun member ord list x =
    1.23 -  (find_index ord list x; true) handle ABSENT _ => false;
    1.24 +fun member ord list x = find_index ord list x > 0;
    1.25  
    1.26  fun insert ord x list =
    1.27    let
    1.28 -    fun insrt 0 ys = x :: ys
    1.29 +    fun insrt 1 ys = x :: ys
    1.30        | insrt i (y :: ys) = y :: insrt (i - 1) ys;
    1.31 -  in (find_index ord list x; list) handle ABSENT i => insrt i list end;
    1.32 +    val idx = find_index ord list x;
    1.33 +  in if idx > 0 then list else insrt (~ idx) list end;
    1.34  
    1.35  fun remove ord x list =
    1.36    let
    1.37 -    fun rmove 0 (_ :: ys) = ys
    1.38 +    fun rmove 1 (_ :: ys) = ys
    1.39        | rmove i (y :: ys) = y :: rmove (i - 1) ys;
    1.40 -  in rmove (find_index ord list x) list handle ABSENT _ => list end;
    1.41 +    val idx = find_index ord list x;
    1.42 +  in if idx > 0 then rmove idx list else list end;
    1.43  
    1.44  
    1.45  (* lists as sets *)