aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-06-29 15:44:05 +0200
committerPierre-Marie Pédrot2020-06-29 15:44:05 +0200
commitc2b76962b407cac8de4465be1e77cf45ff5822d9 (patch)
tree45ab38a3e6c29e73e9c0e7849f69cb07e34a700f /ide
parent1221b56974398d96a7df833e7b32d4b7bc044338 (diff)
parenta6571b3ef7a13e996fbb07fbf7758aa7b3cc6a65 (diff)
Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()
Reviewed-by: ppedrot
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide/coq_lex.mll20
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