--- a/src/Pure/Syntax/scan.ML Wed May 20 18:56:59 1998 +0200
+++ b/src/Pure/Syntax/scan.ML Wed May 20 18:57:16 1998 +0200
@@ -47,9 +47,12 @@
-> 'b * 'a list -> 'c * ('d * 'a list)
val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
val error: ('a -> 'b) -> 'a -> 'b
- val source: string -> (string -> 'a -> 'b list * 'a) ->
+ val source': string -> (string -> 'a -> 'b list * 'a) ->
('b list * 'a -> 'c) -> 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
'd * 'a -> 'e list * ('d * 'c)
+ val source: string -> (string -> 'a -> 'b list * 'a) ->
+ ('b list * 'a -> 'c) -> 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
+ 'a -> 'd list * 'c
val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
type lexicon
@@ -176,7 +179,7 @@
(* infinite scans -- draining state-based source *)
-fun source def_prmpt get unget stopper scan (state, src) =
+fun source' def_prmpt get unget stopper scan (state, src) =
let
fun drain (xs, s) =
(scan (state, xs), s) handle MORE prmpt =>
@@ -192,6 +195,10 @@
(ys, (state', unget (rest, src')))
end;
+fun source def_prmpt get unget stopper scan src =
+ let val (ys, ((), src')) = source' def_prmpt get unget stopper (lift scan) ((), src)
+ in (ys, src') end;
+
fun single scan = scan >> (fn x => [x]);
fun bulk scan = scan -- repeat (try scan) >> (op ::);