Avoid lookup up too many characters.

This would cause issues in noninteractive mode. For example, when using
Drop, the first character of the OCaml code would be read by Coq's REPL
instead of OCaml's REPL.

The peek_string function is quite inefficient, since the Stream module
does not provide any good function to lookup arbitrary characters (or to
push back characters).

1 files changed, 14 insertions, 3 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 688a76c49c..f485970eec 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -580,15 +580,26 @@ let parse_quotation loc bp s =
       let loc = quotation loc 0 in
       Buffer.contents b, set_loc_pos loc bp (Stream.count s)
 
+let peek_string v s =
+  let l = String.length v in
+  let rec aux i =
+    if Int.equal i l then true
+    else
+      let l' = Stream.npeek (i + 1) s in
+      match List.nth l' i with
+      | c -> Char.equal c v.[i] && aux (i + 1)
+      | exception _ -> false (* EOF *) in
+  aux 0
 
 let find_keyword loc id bp s =
-  match Stream.npeek 3 s with
-  | [':'; '{'; '{'] ->
+  if peek_string ":{{" s then
+    begin
       (* "xxx:{{" always starts a sentence-gobbling quotation, whether registered or not *)
       Stream.junk s;
       let txt, loc = parse_quotation loc bp s in
       QUOTATION (id ^ ":", txt), loc
-  | _ ->
+    end
+  else
   let tt = ttree_find !token_tree id in
   match progress_further loc tt.node 0 tt s with
   | None -> raise Not_found