Merge branch 'fix/andre/boris-feedback-open62541' into 'master'

Fix/andre/boris feedback open62541

See merge request frama-c/frama-c!2632

doc/userman/user-sources.tex

@@ -98,7 +98,9 @@ the compilation database and include associated preprocessing flags,
 as if they had been manually added via \texttt{-cpp-extra-args-per-file}.
 Note: if both \texttt{-cpp-extra-args-per-file} and the JSON compilation
 database specify options for a given file, the former are used and the latter
-are ignored.
+are ignored. Also note that the use of the database simply adds flags
+{\em for the files specified in the command-line}, but these files must still
+be specified by the user.
 
 In all of the above cases,
 \acsl annotations are pre-processed by default (option \optiondef{-}{pp-annot}

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,