# HG changeset patch # User wenzelm # Date 894558888 -7200 # Node ID 0f56199a8d97fd2dc5de8bb0a642a06b7f23384e # Parent 8fbccead369532901542ef9c4c8c499dba0d2fc7 improved source: state-based; tuned bulk; diff -r 8fbccead3695 -r 0f56199a8d97 src/Pure/Syntax/scan.ML --- a/src/Pure/Syntax/scan.ML Thu May 07 18:05:46 1998 +0200 +++ b/src/Pure/Syntax/scan.ML Thu May 07 18:34:48 1998 +0200 @@ -45,10 +45,9 @@ -> 'b * ''a list -> 'c * ('d * ''a list) val finite: ''a -> (''a list -> 'b * ''a list) -> ''a list -> 'b * ''a list val error: ('a -> 'b) -> 'a -> 'b - val source: string -> (string -> 'a -> 'b list * 'a) - -> ('c * 'a -> 'd) -> ('b list -> 'e * 'c) -> 'a -> 'e * 'd - val single: ('a -> 'b * 'c) -> 'a -> 'b list * 'c - val many: ('a -> 'b * 'a) -> 'a -> 'b list * 'a + val source: string -> (string -> 'a -> 'b list * 'a) -> + ('c * 'a -> 'd) -> ('e * 'b list -> 'f * ('g * 'c)) -> 'e * 'a -> 'f * ('g * 'd) + val bulk: bool -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a type lexicon val dest_lexicon: lexicon -> string list list val make_lexicon: string list list -> lexicon @@ -169,22 +168,23 @@ in (y, xs') end; -(* infinite scans *) +(* infinite scans -- draining state-based source *) -fun source def_prmpt get unget scan src = +fun source def_prmpt get unget scan (state, src) = let fun drain (xs, s) = - (scan xs, s) + (scan (state, xs), s) handle MORE prmpt => - let val (more_xs, s') = get (if_none prmpt def_prmpt) s in - if null more_xs then raise ABORT "Input source exhausted" - else drain (xs @ more_xs, s') + let val (xs', s') = get (if_none prmpt def_prmpt) s in + if null xs' then raise ABORT "Input source exhausted" + else drain (xs @ xs', s') end; - val ((ys, xs'), src') = drain (get def_prmpt src); - in (ys, unget (xs', src')) end; + val ((ys, (state', rest)), src') = drain (get def_prmpt src); + in (ys, (state', unget (rest, src'))) end; fun single scan = scan >> (fn x => [x]); fun many scan = scan -- repeat (try scan) >> (op ::); +fun bulk do_many = if do_many then many else single;