diff options
| author | Pierre-Marie Pédrot | 2020-06-29 15:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:44:05 +0200 |
| commit | c2b76962b407cac8de4465be1e77cf45ff5822d9 (patch) | |
| tree | 45ab38a3e6c29e73e9c0e7849f69cb07e34a700f | |
| parent | 1221b56974398d96a7df833e7b32d4b7bc044338 (diff) | |
| parent | a6571b3ef7a13e996fbb07fbf7758aa7b3cc6a65 (diff) | |
Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()
Reviewed-by: ppedrot
| -rw-r--r-- | ide/coqide/coq_lex.mll | 20 |
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 |
