CoqIDE: fix lexing of UTF-8 in quotations like constr:()

1 files changed, 16 insertions, 4 deletions

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