src/Pure/Syntax/scan.ML
changeset 5869 b279a84ac11c
parent 5861 7536314d9a5f
child 5987 389d03e6e093
equal deleted inserted replaced
5868:0022d0a913b5 5869:b279a84ac11c
    46   val force: ('a -> 'b) -> 'a -> 'b
    46   val force: ('a -> 'b) -> 'a -> 'b
    47   val prompt: string -> ('a -> 'b) -> 'a -> 'b
    47   val prompt: string -> ('a -> 'b) -> 'a -> 'b
    48   val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    48   val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    49     -> 'b * 'a list -> 'c * ('d * 'a list)
    49     -> 'b * 'a list -> 'c * ('d * 'a list)
    50   val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    50   val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
       
    51   val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    51   val catch: ('a -> 'b) -> 'a -> 'b
    52   val catch: ('a -> 'b) -> 'a -> 'b
    52   val error: ('a -> 'b) -> 'a -> 'b
    53   val error: ('a -> 'b) -> 'a -> 'b
    53   val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    54   val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    54     'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    55     'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    55     ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
    56     ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
   184 
   185 
   185 fun finite stopper scan xs =
   186 fun finite stopper scan xs =
   186   let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
   187   let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
   187   in (y, xs') end;
   188   in (y, xs') end;
   188 
   189 
       
   190 fun read stopper scan xs =
       
   191   (case error (finite stopper (option scan)) xs of
       
   192     (y as Some _, []) => y
       
   193   | _ => None);
       
   194 
       
   195 
   189 
   196 
   190 (* infinite scans -- draining state-based source *)
   197 (* infinite scans -- draining state-based source *)
   191 
   198 
   192 fun drain def_prmpt get stopper scan ((state, xs), src) =
   199 fun drain def_prmpt get stopper scan ((state, xs), src) =
   193   (scan (state, xs), src) handle MORE prmpt =>
   200   (scan (state, xs), src) handle MORE prmpt =>