Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 15acb65c authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix broken conditional and clean code.

parent 10d1b5f2
No related branches found
No related tags found
No related merge requests found
...@@ -166,13 +166,11 @@ let rec num_lines acc tr = ...@@ -166,13 +166,11 @@ let rec num_lines acc tr =
let rec print_transf fmt depth max_depth provers tr = let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<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\">" fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified) (color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified)
(max_depth - depth + 1); (max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" tr.transf_name ; 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>" fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
done; done;
fprintf fmt "</tr>@\n"; fprintf fmt "</tr>@\n";
...@@ -186,13 +184,10 @@ let rec num_lines acc tr = ...@@ -186,13 +184,10 @@ let rec num_lines acc tr =
and print_goal fmt needs_tr depth max_depth provers g = and print_goal fmt needs_tr depth max_depth provers g =
if needs_tr then fprintf fmt "<tr>"; 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\">" fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g)) (color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
(max_depth - depth + 1); (max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_user_name g); 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); print_results fmt provers (goal_external_proofs g);
fprintf fmt "</tr>@\n"; fprintf fmt "</tr>@\n";
PHstr.iter PHstr.iter
...@@ -201,7 +196,7 @@ let rec num_lines acc tr = ...@@ -201,7 +196,7 @@ let rec num_lines acc tr =
let print_theory fn fmt th = let print_theory fn fmt th =
let depth = theory_depth th in let depth = theory_depth th in
if depth > 0 then if depth > 0 then begin
let provers = Hprover.create 9 in let provers = Hprover.create 9 in
provers_stats provers th; provers_stats provers th;
let provers = let provers =
...@@ -224,13 +219,13 @@ let rec num_lines acc tr = ...@@ -224,13 +219,13 @@ let rec num_lines acc tr =
fprintf fmt "</span></h2>@\n"; fprintf fmt "</span></h2>@\n";
fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth; fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
(* fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>"; *)
List.iter List.iter
(fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr) (fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
provers; provers;
fprintf fmt "</tr>@\n"; fprintf fmt "</tr>@\n";
List.iter (print_goal fmt true 1 depth provers) th.theory_goals; List.iter (print_goal fmt true 1 depth provers) th.theory_goals;
fprintf fmt "</table>@\n" fprintf fmt "</table>@\n"
end
let print_file fmt f = let print_file fmt f =
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *) (* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment