diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 10a4ec0697ffe7c600de4fb8a291f9e07e6d8159..2aa52b66aaa05d4cd82672c4ffc78c03259c395e 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 3d08c1cd3f6977288219889a6c0c9e60f1d39411..1e1d2220129f994acf95965d78108d1b8b650a22 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 864f9647854cd605373bea71078e3501e95a2189..0290a56ff053ceff3bf8b15d39f052a0cec4d1d0 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 *) (* -------------------------------------------------------------------------- *)