Commit 030f79e0 authored by Andrei Paskevich's avatar Andrei Paskevich

minor fixes

parent 26b7cbf9
......@@ -432,6 +432,7 @@ let empty_tool_res =
{tr with timeout = add_nb_avg tr.timeout time}
| Db.Done Call_provers.Invalid ->
{tr with invalid = add_nb_avg tr.invalid time}
| Db.Done Call_provers.OutOfMemory
| Db.Undone | Db.Done (Call_provers.Unknown _) ->
{tr with unknown = add_nb_avg tr.unknown time}
| Db.Done (Call_provers.Failure _)
......
......@@ -477,6 +477,7 @@ let int64_from_status = function
| Done (Call_provers.Failure _) -> 4L
| Done Call_provers.Invalid -> 5L
| Done Call_provers.HighFailure -> 6L
| Done Call_provers.OutOfMemory -> 7L
let status_array = [|
Undone;
......@@ -485,7 +486,9 @@ let status_array = [|
Done (Call_provers.Unknown "");
Done (Call_provers.Failure "");
Done Call_provers.Invalid;
Done Call_provers.HighFailure; |]
Done Call_provers.HighFailure;
Done Call_provers.OutOfMemory;
|]
let status_from_int64 i =
try
......
......@@ -36,7 +36,7 @@ let set_opt_style = function
| "simple" -> opt_style := SimpleTree
| "jstree" -> opt_style := Jstree
| "table" -> opt_style := Table
| _ ->
| _ ->
eprintf "Unknown html style, ignored@."
let () = set_opt_style default_style
......@@ -120,9 +120,9 @@ struct
let print_prover = Whyconf.print_prover
let color_of_status ?(dark=false) fmt b =
fprintf fmt "%s" (if b then
if dark then "008000" else "C0FFC0"
let color_of_status ?(dark=false) fmt b =
fprintf fmt "%s" (if b then
if dark then "008000" else "C0FFC0"
else "FF0000")
let print_results fmt provers proofs =
......@@ -147,9 +147,9 @@ let print_results fmt provers proofs =
| Call_provers.Unknown _ ->
fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
| Call_provers.Failure _ ->
fprintf fmt "FF8000\">Failure "
| Call_provers.HighFailure _ ->
fprintf fmt "FF8000\">High Failure "
fprintf fmt "FF8000\">Failure"
| Call_provers.HighFailure ->
fprintf fmt "FF8000\">High Failure"
end
| S.Undone _ -> fprintf fmt "E0E0E0\">Undone"
| S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
......@@ -159,16 +159,16 @@ let print_results fmt provers proofs =
let rec num_lines acc tr =
List.fold_left
(fun acc g -> 1 +
PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
(fun acc g -> 1 +
PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
g.goal_transformations acc)
acc tr.transf_goals
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 bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) tr.S.transf_verified
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) tr.S.transf_verified
(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 ;
......@@ -187,7 +187,7 @@ let rec num_lines acc tr =
and print_goal fmt is_first depth max_depth provers g =
if not is_first then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) g.S.goal_verified (max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_expl g);
......@@ -208,7 +208,7 @@ let rec num_lines acc tr =
in
let provers = List.sort Whyconf.Prover.compare provers in
let name = th.S.theory_name.Ident.id_string in
fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
(color_of_status ~dark:true) th.S.theory_verified
name (if th.S.theory_verified then "fully verified" else "not fully verified")
;
......
......@@ -45,7 +45,7 @@ let spec =
("-o",
Arg.Set_string opt_output_dir,
"<dir> where to produce LaTeX files (default: session dir)") ::
("-e",
("-e",
Arg.String add_element,
"<path> produce a table for the element denoted by <path>") ::
("-longtable",
......@@ -142,7 +142,8 @@ let print_result_prov proofs prov fmt=
| Call_provers.OutOfMemory -> fprintf fmt "& \\outofmemory "
| Call_provers.Unknown _ -> fprintf fmt "& \\unknown "
| Call_provers.Failure _ -> fprintf fmt "& \\failure "
| Call_provers.HighFailure _ -> fprintf fmt "& \\highfailure "
| Call_provers.HighFailure -> fprintf fmt "& \\highfailure "
end
| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
| Session.Undone _ -> fprintf fmt "& Undone"
......@@ -389,7 +390,7 @@ let element_latex_stat_theory th n table dir e =
| g :: r ->
try
let goals =
List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
th.S.theory_goals
in
let g = List.assoc g goals in
......@@ -423,7 +424,7 @@ let element_latex_stat files n table dir e =
(fun fname file ->
let fname = Filename.basename fname in
let fname = List.hd (Str.split re_dot fname) in
if fname = f then
if fname = f then
begin
found := true;
element_latex_stat_file file n table dir r
......
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