From a5abb5d9c2d8c61be2444b5f5922cf124f98bae0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Sep 2020 14:40:22 +0200
Subject: 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).
---
 parsing/cLexer.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3