src/Pure/General/seq.ML

--- a/src/Pure/General/seq.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/General/seq.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -36,9 +36,12 @@
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
   datatype 'a result = Result of 'a | Error of unit -> string
+  val make_results: 'a seq -> 'a result seq
+  val filter_results: 'a result seq -> 'a seq
   val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq
   val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq
   val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq
+  val first_result: string -> 'a result seq -> 'a * 'a seq
   val the_result: string -> 'a result seq -> 'a
   val succeed: 'a -> 'a seq
   val fail: 'a -> 'b seq
@@ -205,6 +208,9 @@
 
 datatype 'a result = Result of 'a | Error of unit -> string;
 
+fun make_results xq = map Result xq;
+fun filter_results xq = map_filter (fn Result x => SOME x | Error _ => NONE) xq;
+
 fun maps_results f xq =
   make (fn () =>
     (case pull xq of
@@ -216,17 +222,19 @@
 fun map_result f = maps_result (single o f);
 
 (*first result or first error within sequence*)
-fun the_result default_msg seq =
+fun first_result default_msg seq =
   let
     fun result opt_msg xq =
       (case (opt_msg, pull xq) of
-        (_, SOME (Result x, _)) => x
+        (_, SOME (Result x, xq')) => (x, filter_results xq')
       | (SOME _, SOME (Error _, xq')) => result opt_msg xq'
       | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq'
       | (SOME msg, NONE) => error (msg ())
       | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg));
   in result NONE seq end;
 
+fun the_result default_msg seq = #1 (first_result default_msg seq);
+
 
 
 (** sequence functions **)      (*cf. Pure/tactical.ML*)