diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index 045d1ee3d24008dedb4d6ad449bc22da006b158a..48384ab69af7158c3cda769b45026aeb474e3f3b 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 cf1317591f60695924090c66eccaf3871f191ab0..e122cd7f80c852b8d7d42b77b6a68aa2f4a642e0 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}