From 96bdd6de639540fb58b904d01202433df156e0c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 Jan 2025 17:01:01 +0100
Subject: [PATCH] [kernel] Indicates message truncation, and only truncate
messages on terminal.
Rich_text: do not silently truncate buffers, but export function [truncate].
Log: uses [Rich_text.truncate] on messages printed on terminal, and prefix
truncated messages to indicate the truncation.
---
.../plugin_entry_points/log.ml | 12 +++++++
src/libraries/utils/rich_text.ml | 35 ++++++++-----------
src/libraries/utils/rich_text.mli | 4 +++
3 files changed, 31 insertions(+), 20 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 10a4ec0697..2aa52b66aa 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -20,6 +20,9 @@
(* *)
(**************************************************************************)
+(* Messages longer than N characters are truncated when printed on terminal. *)
+let max_message_length = 2097152
+
type kind = Result | Feedback | Debug | Warning | Error | Failure
[@@@ warning "-32"]
@@ -467,6 +470,7 @@ let logtransient channel text =
try
Format.pp_print_newline fmt () ;
Format.pp_print_flush fmt () ;
+ ignore (Rich_text.truncate buffer max_message_length) ;
let p,q = Rich_text.trim buffer in
do_transient channel.terminal (Rich_text.contents buffer) p q ;
close_buffer channel
@@ -497,11 +501,19 @@ let logwithfinal finally channel
Format.pp_close_box fmt () ;
Format.pp_print_newline fmt () ;
Format.pp_print_flush fmt () ;
+ let truncated =
+ if channel.terminal.isatty
+ then Rich_text.truncate buffer max_message_length
+ else false
+ in
let p,q = Rich_text.trim buffer in
let output =
if p <= q then
let source = get_source current source in
let message = Rich_text.range buffer p q in
+ let message =
+ if truncated then "(truncated message) " ^ message else message
+ in
let event = {
evt_kind = kind ;
evt_plugin = channel.plugin ;
diff --git a/src/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index 3d08c1cd3f..1e1d222012 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -106,8 +106,6 @@ let pretty ?vbox fmt message =
(* -------------------------------------------------------------------------- *)
let min_buffer = 128 (* initial size of buffer *)
-let max_buffer = 2097152 (* maximal size of buffer *)
-let tgr_buffer = 3145728 (* elasticity (internal overhead) *)
type buffer = {
mutable formatter : Format.formatter ; (* formatter on self (recursive) *)
@@ -136,7 +134,8 @@ let shrink buffer =
if Buffer.length buffer.content > min_buffer then
Buffer.reset buffer.content
-let truncate_text buffer size =
+let truncate buffer size =
+ let truncated = ref false in
if Buffer.length buffer.content > size then
begin
let p = trim_begin buffer in
@@ -147,23 +146,21 @@ let truncate_text buffer size =
else if n <= size then
Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n
else
- begin
- let n_left = size / 2 - 3 in
- let n_right = size - n_left - 5 in
- if p > 0 then
- Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
- let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
- Buffer.truncate buffer.content n_left;
- Buffer.add_string buffer.content "[...]";
- Buffer.add_string buffer.content buf_right;
- end
- end
+ let n_left = size / 2 - 3 in
+ let n_right = size - n_left - 5 in
+ if p > 0 then
+ Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
+ let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
+ Buffer.truncate buffer.content n_left;
+ Buffer.add_string buffer.content "[...]";
+ Buffer.add_string buffer.content buf_right;
+ truncated := true;
+ end;
+ !truncated
(* All text added shall go through this function *)
let append buffer s k n =
- Buffer.add_substring buffer.content s k n ;
- if Buffer.length buffer.content > tgr_buffer then
- truncate_text buffer max_buffer
+ Buffer.add_substring buffer.content s k n
let push_tag buffer _tag =
let p = Buffer.length buffer.content in
@@ -219,13 +216,12 @@ let create ?indent ?margin () =
buffer
let trim buffer =
- truncate_text buffer max_buffer ;
let p = trim_begin buffer in
let q = trim_end buffer in
p , q
let contents buffer =
- truncate_text buffer max_buffer ; Buffer.contents buffer.content
+ Buffer.contents buffer.content
let message buffer =
( Buffer.contents buffer.content , List.rev buffer.revtags )
@@ -247,7 +243,6 @@ let to_string ?(indent=20) ?(margin=40) ?(trim=true) pp data =
let fmt = formatter buffer in
pp fmt data ;
Format.pp_print_flush fmt () ;
- truncate_text buffer max_buffer ;
if trim then
let p = trim_begin buffer in
let q = trim_end buffer in
diff --git a/src/libraries/utils/rich_text.mli b/src/libraries/utils/rich_text.mli
index 864f964785..0290a56ff0 100644
--- a/src/libraries/utils/rich_text.mli
+++ b/src/libraries/utils/rich_text.mli
@@ -106,6 +106,10 @@ val trim : buffer -> int * int
(** Resize the buffer to roughly fit its actual content. *)
val shrink : buffer -> unit
+(** [truncate buffer size] truncates the content of [buffer] if longer than
+ [size] characters. Returns true if the bufffer has been truncated. *)
+val truncate : buffer -> int -> bool
+
(* -------------------------------------------------------------------------- *)
(** Printer *)
(* -------------------------------------------------------------------------- *)
--
GitLab