From a6c650f9912dd594f25b8a65691b4c9ed76b916b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 28 Apr 2020 10:43:30 +0200
Subject: [PATCH] [Kernel] Compress large contexts in error messages
---
src/kernel_internals/parsing/errorloc.ml | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index 21ccfba0c87..3c439cfe907 100644
--- a/src/kernel_internals/parsing/errorloc.ml
+++ b/src/kernel_internals/parsing/errorloc.ml
@@ -126,8 +126,14 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
| None -> pos.Filepath.pos_lnum, pos.Filepath.pos_lnum
| Some l -> min l pos.Filepath.pos_lnum, max l pos.Filepath.pos_lnum
in
+ (* The difference between the first and last error lines can be very
+ large; in this case, we print only the first and last [error_ctx]
+ lines, with "..." between them. *)
let first_to_print = max (first_error_line-ctx) 1 in
let last_to_print = last_error_line+ctx in
+ let error_ctx = 3 in
+ 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
@@ -148,8 +154,16 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
(* print error lines *)
while !i <= last_error_line do
let line = input_line in_ch in
- error_line_len := String.length line;
- Format.fprintf fmt "%-6d%s\n" !i line;
+ if compress_error && !i = first_error_line + error_ctx then
+ Format.fprintf fmt "%d-%d [... omitted ...]\n"
+ (first_error_line + error_ctx) (last_error_line - error_ctx)
+ else if compress_error && !i > first_error_line + error_ctx &&
+ !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
done;
(* if more than one line of context, print blank line,
--
GitLab