Commit 397e4184 authored by MARCHE Claude's avatar MARCHE Claude

add ellipsis to avoid printing too large terms

parent ed302530
......@@ -490,7 +490,8 @@ let env_session () =
| None -> assert false
| Some e -> e
let task_text t = Pp.string_of Pretty.print_task t
let task_text t =
Pp.string_of ~max_boxes:42 Pretty.print_task t
let split_transformation = "split_goal_wp"
let inline_transformation = "inline_goal"
......
......@@ -166,9 +166,12 @@ let rec print_list_opt sep print fmt = function
notempty1 || notempty2
let string_of p x =
let string_of ?max_boxes p x =
let b = Buffer.create 100 in
let fmt = formatter_of_buffer b in
Opt.iter (fun x ->
Format.pp_set_ellipsis_text fmt "...";
Format.pp_set_max_boxes fmt x) max_boxes;
fprintf fmt "%a@?" p x;
Buffer.contents b
......
......@@ -133,7 +133,9 @@ val print_list_opt :
(formatter -> 'a -> bool) -> formatter -> 'a list -> bool
val string_of : (Format.formatter -> 'a -> unit) -> 'a -> string
val string_of : ?max_boxes:int ->
(Format.formatter -> 'a -> unit) -> 'a -> string
val string_of_wnl : (Format.formatter -> 'a -> unit) -> 'a -> string
(** same as {!string_of} but without newline *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment