From 89caa99ed29ff4844105044e2b8976cb77f6b39a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 14 Jan 2020 19:05:49 +0100
Subject: [PATCH] [lexer] more accurate lexing of filenames in #line directives
---
src/kernel_internals/parsing/clexer.mll | 4 +++-
src/kernel_internals/parsing/logic_lexer.mll | 17 +++++++++--------
2 files changed, 12 insertions(+), 9 deletions(-)
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 045d1ee3d24..48384ab69af 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -742,7 +742,9 @@ and file = parse
| '"' ([^ '\012' '\t' '"']* as d) "//\"" {
E.setCurrentWorkingDirectory d;
endline lexbuf }
-| '"' ([^ '\012' '\t' '"']* as f) '"' {
+| '"' (([^ '\012' '\t' '"']|"\\\"")* as f) '"' {
+ let unescape = Str.regexp_string "\\\"" in
+ let f = Str.global_replace unescape "\"" f in
E.setCurrentFile f;
endline lexbuf}
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index cf1317591f6..e122cd7f80c 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -446,14 +446,15 @@ and hash = parse
and file = parse
'\n' { update_newline_loc lexbuf; token lexbuf}
| [' ''\t''\r'] { file lexbuf}
-| '"' [^ '\012' '\t' '"']* '"'
- {
- let n = Lexing.lexeme lexbuf in
- let n1 = String.sub n 1
- ((String.length n) - 2) in
- update_file_loc lexbuf n1;
- endline lexbuf
- }
+| '"' ([^ '\012' '\t' '"']|"\\\"")* '"' {
+ let n = Lexing.lexeme lexbuf in
+ let n1 = String.sub n 1
+ ((String.length n) - 2) in
+ let unescape = Str.regexp_string "\\\"" in
+ let n1 = Str.global_replace unescape "\"" n1 in
+ update_file_loc lexbuf n1;
+ endline lexbuf
+ }
| _ { endline lexbuf}
--
GitLab