From 27a156f05e40d670f36d51ca4727929b3a79b744 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 3 Sep 2019 13:56:33 +0200
Subject: [PATCH] [Parsing] Fixes location of errors for ghost else with
comments
---
src/kernel_internals/parsing/clexer.mll | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 808202db908..bee01ad76aa 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -347,6 +347,10 @@ let lex_comment remainder buffer lexbuf =
(match buffer with None -> () | Some b -> Buffer.add_string b s) ;
remainder buffer lexbuf
+let error_count_lines comments =
+ let newline_if_n c = if c = '\n' then E.newline () in
+ String.iter newline_if_n comments
+
let do_lex_comment ?(first_string="") remainder lexbuf =
let buffer =
if Kernel.PrintComments.get () then begin
@@ -809,11 +813,13 @@ and msasmnobrace = parse
cur ^ (msasmnobrace lexbuf) }
and annot_first_token = parse
- | "ghost" (blank| '\n' | ("//" [^'\n']* '\n') )* "else" {
+ | "ghost" ((blank| '\n' | ("//" [^'\n']* '\n') )* as comments) "else" {
if is_oneline_ghost () then E.parse_error "nested ghost code";
Buffer.clear buf;
+ let loc = currentLoc () in
+ error_count_lines comments ;
enter_ghost_code ();
- LGHOST_ELSE (currentLoc ())
+ LGHOST_ELSE (loc)
}
| "ghost" {
if is_oneline_ghost () then E.parse_error "nested ghost code";
--
GitLab