--- a/src/Pure/General/table.ML Tue Jul 08 23:20:07 2008 +0200
+++ b/src/Pure/General/table.ML Wed Jul 09 17:14:31 2008 +0200
@@ -27,10 +27,11 @@
val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a
val dest: 'a table -> (key * 'a) list
val keys: 'a table -> key list
+ val exists: (key * 'a -> bool) -> 'a table -> bool
+ val forall: (key * 'a -> bool) -> 'a table -> bool
+ val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
val min_key: 'a table -> key option
val max_key: 'a table -> key option
- val exists: (key * 'a -> bool) -> 'a table -> bool
- val forall: (key * 'a -> bool) -> 'a table -> bool
val defined: 'a table -> key -> bool
val lookup: 'a table -> key -> 'a option
val update: (key * 'a) -> 'a table -> 'a table
@@ -125,15 +126,19 @@
fun dest tab = rev (fold_table cons tab []);
fun keys tab = rev (fold_table (cons o #1) tab []);
-local exception TRUE in
+fun get_first f tab =
+ let
+ exception FOUND of 'b option;
+ fun get entry () = (case f entry of NONE => () | some => raise FOUND some);
+ in (fold_table get tab (); NONE) handle FOUND res => res end;
-fun exists pred tab =
- (fold_table (fn p => fn () => if pred p then raise TRUE else ()) tab (); false)
- handle TRUE => true;
+fun exists pred =
+ is_some o get_first (fn entry => if pred entry then SOME () else NONE);
fun forall pred = not o exists (not o pred);
-end;
+
+(* min/max keys *)
fun min_key Empty = NONE
| min_key (Branch2 (Empty, (k, _), _)) = SOME k