# HG changeset patch
# User wenzelm
# Date 911209268 -3600
# Node ID b279a84ac11cc703bba8dababb67a2a118c1ceb4
# Parent  0022d0a913b5e462a92ddc40d6cc0680f87407ab
added read;

diff -r 0022d0a913b5 -r b279a84ac11c src/Pure/Syntax/scan.ML
--- a/src/Pure/Syntax/scan.ML	Mon Nov 16 10:40:23 1998 +0100
+++ b/src/Pure/Syntax/scan.ML	Mon Nov 16 10:41:08 1998 +0100
@@ -48,6 +48,7 @@
   val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
     -> 'b * 'a list -> 'c * ('d * 'a list)
   val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
+  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
   val catch: ('a -> 'b) -> 'a -> 'b
   val error: ('a -> 'b) -> 'a -> 'b
   val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
@@ -186,6 +187,12 @@
   let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
   in (y, xs') end;
 
+fun read stopper scan xs =
+  (case error (finite stopper (option scan)) xs of
+    (y as Some _, []) => y
+  | _ => None);
+
+
 
 (* infinite scans -- draining state-based source *)