From a6571b3ef7a13e996fbb07fbf7758aa7b3cc6a65 Mon Sep 17 00:00:00 2001
From: James Lottes
Date: Tue, 23 Jun 2020 01:11:18 -0700
Subject: CoqIDE: fix lexing of UTF-8 in quotations like constr:()

---
 ide/coqide/coq_lex.mll | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

(limited to 'ide')

diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll
index fe9f108a94..a65954d566 100644
--- a/ide/coqide/coq_lex.mll
+++ b/ide/coqide/coq_lex.mll
@@ -50,7 +50,10 @@ and comment = parse
   | utf8_extra_byte { incr utf8_adjust; comment lexbuf }
   | _ { comment lexbuf }
 
-and quotation o c n l = parse | eof { raise Unterminated } | _ {
+and quotation o c n l = parse
+| eof { raise Unterminated }
+| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
+| _ {
   let x = Lexing.lexeme lexbuf in
   if x = o then quotation_nesting o c n l 1 lexbuf
   else if x = c then
@@ -59,7 +62,10 @@ and quotation o c n l = parse | eof { raise Unterminated } | _ {
   else quotation o c n l lexbuf
 }
 
-and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ {
+and quotation_nesting o c n l v = parse
+| eof { raise Unterminated }
+| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
+| _ {
   let x = Lexing.lexeme lexbuf in
   if x = o then
     if n = v+1 then quotation o c n (l+1) lexbuf
@@ -68,7 +74,10 @@ and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ {
   else quotation o c n l lexbuf
 }
 
-and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ {
+and quotation_closing o c n l v = parse
+| eof { raise Unterminated }
+| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
+| _ {
   let x = Lexing.lexeme lexbuf in
   if x = c then
     if n = v+1 then
@@ -79,7 +88,10 @@ and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ {
   else quotation o c n l lexbuf
 }
 
-and quotation_start o c n = parse | eof { raise Unterminated } | _ {
+and quotation_start o c n = parse
+| eof { raise Unterminated }
+| utf8_extra_byte { incr utf8_adjust; quotation o c n 1 lexbuf }
+| _ {
   let x = Lexing.lexeme lexbuf in
   if x = o then quotation_start o c (n+1) lexbuf
   else quotation o c n 1 lexbuf
-- 
cgit v1.2.3