From 0141f076c2b35f0f6b6bb4db1d274ad99bfaa846 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 29 Apr 2021 11:27:26 +0200
Subject: [PATCH] Do not print tasks when only one is present.
---
engine.ml | 14 +++++++++++---
1 file changed, 11 insertions(+), 3 deletions(-)
diff --git a/engine.ml b/engine.ml
index e86821d..f871123 100644
--- a/engine.ml
+++ b/engine.ml
@@ -254,12 +254,20 @@ let pretty_summary tasks_htbl =
in
Format.fprintf fmt "@[-- %s: @[<hov>%s@]@]" id result_string
in
+ let pretty_tasks _fmt = function
+ | [] | [ _ ] ->
+ (* We don't print task details: the consolidated goal result is enough. *)
+ ()
+ | tasks ->
+ Format.printf "@ %a"
+ (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
+ tasks
+ in
let pretty_goal_tasks fmt (goalname, (consolidated_result, tasks)) =
- Format.fprintf fmt "@[- %s: @[<v>%a@ %a@]@]"
+ Format.fprintf fmt "@[<v 2>- %s: @[%a@]%a@]"
goalname
Solver.Result.pretty (Option.value_exn consolidated_result)
- (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
- tasks
+ pretty_tasks tasks
in
Logs.app (fun m ->
m "@[<v 2>Summary:@ %a@]"
--
GitLab