src/Pure/Syntax/scan.ML
changeset 5861 7536314d9a5f
parent 5048 2af6b01e7ab6
child 5869 b279a84ac11c
equal deleted inserted replaced
5860:ed11c9890852 5861:7536314d9a5f
    35   val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    35   val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    36   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    36   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    37   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    37   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    38   val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
    38   val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
    39   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
    39   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
       
    40   val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
       
    41   val first: ('a -> 'b) list -> 'a -> 'b
    40   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
    42   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
    41   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    43   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    42   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    44   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    43   val try: ('a -> 'b) -> 'a -> 'b
    45   val try: ('a -> 'b) -> 'a -> 'b
    44   val force: ('a -> 'b) -> 'a -> 'b
    46   val force: ('a -> 'b) -> 'a -> 'b
   130   | ((Some tok1, xs1'), (Some tok2, xs2')) =>
   132   | ((Some tok1, xs1'), (Some tok2, xs2')) =>
   131       if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
   133       if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
   132 
   134 
   133 fun ahead scan xs = (fst (scan xs), xs);
   135 fun ahead scan xs = (fst (scan xs), xs);
   134 
   136 
       
   137 fun unless test scan =
       
   138   ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
       
   139 
       
   140 fun first [] = fail
       
   141   | first (scan :: scans) = scan || first scans;
       
   142 
   135 
   143 
   136 (* state based scanners *)
   144 (* state based scanners *)
   137 
   145 
   138 fun depend scan (st, xs) =
   146 fun depend scan (st, xs) =
   139   let val ((st', y), xs') = scan st xs
   147   let val ((st', y), xs') = scan st xs