# HG changeset patch
# User wenzelm
# Date 895683436 -7200
# Node ID 78ff4a45a822a338d0a7e827ea6324c14de46681
# Parent  addfa29d0481a7081060422f9988c9576ed3857f
source vs. source';

diff -r addfa29d0481 -r 78ff4a45a822 src/Pure/Syntax/scan.ML
--- 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 ::);