diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll index fe9f108a9428..a65954d5669d 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