1 files changed, 60 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 63181bc0bc..398899aad4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -118,6 +118,64 @@ struct
 
 end
 
+module Lookahead =
+struct
+
+  let err () = raise Stream.Failure
+
+  type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
+
+  let rec contiguous tok n m =
+    n == m ||
+    let (_, ep) = Loc.unloc (tok n) in
+    let (bp, _) = Loc.unloc (tok (n + 1)) in
+    Int.equal ep bp && contiguous tok (succ n) m
+
+  let check_no_space tok m strm =
+    let n = Stream.count strm in
+    if contiguous tok n (n+m-1) then Some m else None
+
+  let to_entry s (lk : t) =
+    let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
+    Entry.of_parser s run
+
+  let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> None
+  | Some n -> lk2 tok n strm
+
+  let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> lk2 tok n strm
+  | Some n -> Some n
+
+  let lk_empty tok n strm = Some n
+
+  let lk_kw kw tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw' | Tok.IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
+  | _ -> None
+
+  let lk_kws kws tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw | Tok.IDENT kw -> if List.mem_f String.equal kw kws then Some (n + 1) else None
+  | _ -> None
+
+  let lk_ident tok n strm = match stream_nth n strm with
+  | Tok.IDENT _ -> Some (n + 1)
+  | _ -> None
+
+  let lk_ident_except idents tok n strm = match stream_nth n strm with
+  | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1)
+  | _ -> None
+
+  let lk_nat tok n strm = match stream_nth n strm with
+  | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+  | _ -> None
+
+  let rec lk_list lk_elem n strm =
+    ((lk_elem >> lk_list lk_elem) <+> lk_empty) n strm
+
+  let lk_ident_list = lk_list lk_ident
+
+end
+
 (** Grammar extensions *)
 
 (** NB: [extend_statement =
@@ -627,9 +685,9 @@ let with_grammar_rule_protection f x =
   let fs = freeze ~marshallable:false in
   try let a = f x in unfreeze fs; a
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     let () = unfreeze fs in
-    iraise reraise
+    Exninfo.iraise reraise
 
 (** Registering grammar of generic arguments *)