From ce306b36b849e67e672e2df3285e2261dc8f73a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 24 Oct 2019 19:21:02 +0200
Subject: [PATCH] [wp] beautify list of provers
---
src/plugins/wp/register.ml | 15 ++++++++-------
1 file changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 3f93fa21f7a..bbf63ea8913 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -905,15 +905,16 @@ let do_prover_detect () =
else
let open Why3.Whyconf in
let shortcuts = get_prover_shortcuts (Why3Provers.config ()) in
+ let print_prover_shortcuts_for fmt p =
+ Why3.Wstdlib.Mstr.iter
+ (fun name p' -> if Prover.equal p p' then
+ Format.fprintf fmt "%s|" name)
+ shortcuts in
List.iter
(fun p ->
- Wp_parameters.result "Prover %10s %-10s %s [%t%a]"
- p.prover_name p.prover_version p.prover_altern
- (fun fmt ->
- Why3.Wstdlib.Mstr.iter
- (fun name p' -> if Prover.equal p p' then
- Format.fprintf fmt "%s," name)
- shortcuts)
+ Wp_parameters.result "Prover %10s %-6s [%a%a]"
+ p.prover_name p.prover_version
+ print_prover_shortcuts_for p
print_prover_parseable_format p
) provers
--
GitLab