Commit 39ffe0f5 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Backport fixes to why3doc.

parent 857aea61
...@@ -117,7 +117,7 @@ struct ...@@ -117,7 +117,7 @@ struct
let print_results fmt provers proofs = let print_results fmt provers proofs =
List.iter (fun p -> List.iter (fun p ->
fprintf fmt "<td bgcolor=\"#"; fprintf fmt "<td style=\"background-color:#";
begin begin
try try
let pr = S.PHprover.find proofs p in let pr = S.PHprover.find proofs p in
...@@ -167,27 +167,27 @@ let rec num_lines acc tr = ...@@ -167,27 +167,27 @@ 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; for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td bgcolor=\"#%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; *) (* 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 (* depth *) to (*max_depth - 1 + *) List.length provers do
fprintf fmt "<td bgcolor=\"#E0E0E0\"></td>" fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
done; done;
fprintf fmt "</tr>@\n"; fprintf fmt "</tr>@\n";
fprintf fmt "<td rowspan=\"%d\">&nbsp;&nbsp;</td>" (num_lines 0 tr); fprintf fmt "<tr><td rowspan=\"%d\">&nbsp;&nbsp;</td>" (num_lines 0 tr);
let (_:bool) = List.fold_left let (_:bool) = List.fold_left
(fun is_first g -> (fun needs_tr g ->
print_goal fmt is_first (depth+1) max_depth provers g; print_goal fmt needs_tr (depth+1) max_depth provers g;
false) true)
true tr.transf_goals false tr.transf_goals
in () in ()
and print_goal fmt is_first depth max_depth provers g = and print_goal fmt needs_tr depth max_depth provers g =
if not is_first then fprintf fmt "<tr>"; if needs_tr then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *) (* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td bgcolor=\"#%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; *) (* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
...@@ -214,21 +214,21 @@ let rec num_lines acc tr = ...@@ -214,21 +214,21 @@ let rec num_lines acc tr =
String.concat "." ([fn]@l@[t]) String.concat "." ([fn]@l@[t])
with Not_found -> fn ^ "." ^ th.theory_name.Ident.id_string with Not_found -> fn ^ "." ^ th.theory_name.Ident.id_string
in in
fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": " fprintf fmt "<h2><span style=\"color:#%a\">Theory \"%s\": "
(color_of_status ~dark:true) (Opt.inhabited th.S.theory_verified) (color_of_status ~dark:true) (Opt.inhabited th.S.theory_verified)
name; name;
begin match th.S.theory_verified with begin match th.S.theory_verified with
| Some t -> fprintf fmt "fully verified in %.02f s" t | Some t -> fprintf fmt "fully verified in %.02f s" t
| None -> fprintf fmt "not fully verified" | None -> fprintf fmt "not fully verified"
end; end;
fprintf fmt "</font></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>"; *) (* 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 "</td></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"
...@@ -246,18 +246,19 @@ let rec num_lines acc tr = ...@@ -246,18 +246,19 @@ let rec num_lines acc tr =
print_file) s.session_files print_file) s.session_files
let context : context = "<!DOCTYPE html\ let context : context = "<!DOCTYPE html \
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\ \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\ \n<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\ \n<head>\
<title>Why3 session of %s</title>\ \n <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />\
</head>\ \n <title>Why3 session of %s</title>\
<body>\ \n</head>\
%a\ \n<body>\
</body>\ \n%a\
</html>\ \n</body>\
" \n</html>\
\n"
let run_one = run_file context print_session let run_one = run_file context print_session
...@@ -314,18 +315,19 @@ struct ...@@ -314,18 +315,19 @@ struct
print_file) s.session_files print_file) s.session_files
let context : context = "<!DOCTYPE html\ let context : context = "<!DOCTYPE html \
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\ \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\ \n<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\ \n<head>\
<title>Why3 session of %s</title>\ \n <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />\
</head>\ \n <title>Why3 session of %s</title>\
<body>\ \n</head>\
%a\ \n<body>\
</body>\ \n%a\
</html>\ \n</body>\
" \n</html>\
\n"
let run_one = run_file context print_session let run_one = run_file context print_session
......
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