From 15acb65c18931bb55d85d0e7fb8aafb7e213462c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 16 May 2018 17:05:50 +0200
Subject: [PATCH] Fix broken conditional and clean code.
---
src/why3session/why3session_html.ml | 11 +++--------
1 file changed, 3 insertions(+), 8 deletions(-)
diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml
index c3e647d6b4..b789ce9fc9 100644
--- a/src/why3session/why3session_html.ml
+++ b/src/why3session/why3session_html.ml
@@ -166,13 +166,11 @@ let rec num_lines acc tr =
let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<tr>";
- for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified)
(max_depth - depth + 1);
- (* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf fmt "%s</td>" tr.transf_name ;
- for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
+ for _i=1 to List.length provers do
fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
done;
fprintf fmt "</tr>@\n";
@@ -186,13 +184,10 @@ let rec num_lines acc tr =
and print_goal fmt needs_tr depth max_depth provers g =
if needs_tr then fprintf fmt "<tr>";
- (* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
(max_depth - depth + 1);
- (* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf fmt "%s</td>" (S.goal_user_name g);
-(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results fmt provers (goal_external_proofs g);
fprintf fmt "</tr>@\n";
PHstr.iter
@@ -201,7 +196,7 @@ let rec num_lines acc tr =
let print_theory fn fmt th =
let depth = theory_depth th in
- if depth > 0 then
+ if depth > 0 then begin
let provers = Hprover.create 9 in
provers_stats provers th;
let provers =
@@ -224,13 +219,13 @@ let rec num_lines acc tr =
fprintf fmt "</span></h2>@\n";
fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
- (* fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>"; *)
List.iter
(fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
provers;
fprintf fmt "</tr>@\n";
List.iter (print_goal fmt true 1 depth provers) th.theory_goals;
fprintf fmt "</table>@\n"
+ end
let print_file fmt f =
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
--
GitLab