From bf3abe67aba004b6dfa1238e2b6338a1da679b37 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Jan 2024 15:34:48 +0100
Subject: [PATCH] [kernel] better pp_context
---
src/kernel_internals/parsing/errorloc.ml | 13 ++++++++-----
src/kernel_internals/parsing/errorloc.mli | 6 +++++-
src/plugins/aorai/utils_parser.ml | 3 ++-
3 files changed, 15 insertions(+), 7 deletions(-)
diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index b214658b0ff..c1a5effb6b7 100644
--- a/src/kernel_internals/parsing/errorloc.ml
+++ b/src/kernel_internals/parsing/errorloc.ml
@@ -142,7 +142,7 @@ let setCurrentFile n =
plus up to [ctx] lines before and after [pos.pos_lnum] (if they exist),
similar to 'grep -C<ctx>'. The first line is numbered 1.
Most exceptions are silently caught and printing is stopped if they occur. *)
-let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
+let pp_context_from_file ?(ctx=2) ?start_line ?(start_char=1) fmt pos =
try
let in_ch = open_in (pos.Filepath.pos_path :> string) in
try
@@ -161,7 +161,6 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
let error_height = last_error_line - first_error_line + 1 in
let compress_error = error_height > 2 * error_ctx + 1 + 2 in
let i = ref 1 in
- let error_line_len = ref 0 in
try
(* advance to line *)
while !i < first_to_print do
@@ -187,7 +186,6 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
!i <= last_error_line - error_ctx then
() (* ignore line *)
else begin
- error_line_len := String.length line;
Format.fprintf fmt "%-6d%s\n" !i line;
end;
incr i
@@ -199,7 +197,8 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
else begin
let cursor =
String.make 6 ' ' ^
- String.make !error_line_len '^'
+ String.make (start_char - 1) ' ' ^
+ String.make (pos.pos_cnum - pos.pos_bol - start_char + 1) '^'
in
Format.fprintf fmt "%s\n" cursor
end;
@@ -293,7 +292,11 @@ let parse_error ?source msg =
pp_location (start_pos, last_pos)
pretty_token (Lexing.lexeme current.lexbuf);
Format.fprintf fmt "%a@."
- (pp_context_from_file ~start_line:start_pos.Filepath.pos_lnum ~ctx:2) last_pos);
+ (pp_context_from_file
+ ~start_line:start_pos.Filepath.pos_lnum
+ ~ctx:2
+ ~start_char:(start_pos.pos_cnum - start_pos.pos_bol + 1))
+ last_pos);
raise (Log.AbortError "kernel"))
msg
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index 2935d535720..3d2163ab129 100644
--- a/src/kernel_internals/parsing/errorloc.mli
+++ b/src/kernel_internals/parsing/errorloc.mli
@@ -70,9 +70,13 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and
of context before and after. [ctx] defaults to 2.
If [start_line] is specified, then all lines between [start_line] and
[pos.pos_lnum] are considered part of the error.
+ If [start_line] and [pos.pos_lnum] are identical (or [start_line] is None),
+ the portion of the line between [start_char] (defaults to 1) and
+ the character position indicated by [pos] is underlined with [^].
*)
val pp_context_from_file:
- ?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit
+ ?ctx:int -> ?start_line:int -> ?start_char:int ->
+ Format.formatter -> Filepath.position -> unit
(** prints a readable description of a location
@since 22.0-Titanium *)
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index e12815ab464..52cfe20c61e 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -30,10 +30,11 @@ let current_loc lex = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
let abort_current lex fmt =
let source = current_loc lex in
let start_line = source.Filepath.pos_lnum in
+ let start_char = source.pos_cnum - source.pos_bol in
let fmt = "before or at token %s@\n%a@\n" ^^ fmt in
Aorai_option.abort ~source fmt
(Lexing.lexeme lex)
- (Errorloc.pp_context_from_file ~start_line ~ctx:2) source
+ (Errorloc.pp_context_from_file ~start_line ~start_char ~ctx:2) source
let unknown_token lex =
abort_current lex
--
GitLab