Commit b8291e85 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix output of transformation arguments and factor some common code.

parent a9741e53
......@@ -153,9 +153,7 @@ let rec num_lines s acc tr =
fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (tn_proved s tr)
(max_depth - depth + 1);
let name = (get_transf_name s tr) ^
(String.concat "" (get_transf_args s tr)) in
fprintf fmt "%s</td>" name ;
fprintf fmt "%s</td>" (get_transf_string s tr);
for _i=1 to List.length provers do
fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
done;
......@@ -264,10 +262,8 @@ struct
print_proof_status pa.proof_state
let rec print_transf s fmt tr =
let name = (get_transf_name s tr) ^
(String.concat "" (get_transf_args s tr)) in
fprintf fmt "<li>%s : <ul>%a</ul></li>"
name
(get_transf_string s tr)
(Pp.print_list Pp.newline (print_goal s)) (get_sub_tasks s tr)
and print_goal s fmt g =
......
......@@ -182,8 +182,7 @@ let rec stats_of_goal ~root prefix_name stats ses goal =
end
and stats_of_transf prefix_name stats ses transf =
let prefix_name = prefix_name ^ (get_transf_name ses transf) ^
(String.concat "" (get_transf_args ses transf)) ^ " / " in
let prefix_name = prefix_name ^ (get_transf_string ses transf) ^ " / " in
List.iter (stats_of_goal ~root:false prefix_name stats ses) (get_sub_tasks ses transf)
let stats_of_theory file stats ses theory =
......@@ -262,9 +261,7 @@ let rec print_goal_stats ~time depth ses (g,l) =
and print_transf_stats ~time depth ses (tr,l) =
for _i=1 to depth do printf " " done;
let name = (get_transf_name ses tr) ^
(String.concat "" (get_transf_args ses tr)) in
printf "+-- transformation %s@\n" name;
printf "+-- transformation %s@\n" (get_transf_string ses tr);
List.iter (print_goal_stats ~time (depth+1) ses) l
let stats2_of_theory ~nb_proofs ses th =
......
......@@ -246,8 +246,7 @@ let rec goal_latex2_stat s fmt prov depth depth_max subgoal g =
begin
List.iter
(fun tr ->
let name = (get_transf_name s tr) ^
(String.concat "" (get_transf_args s tr)) in
let name = get_transf_string s tr in
style_2_row fmt ~transf:true (depth+1) prov subgoal
(protect name);
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\@."
......
......@@ -330,6 +330,8 @@ let get_used_provers session =
session;
!sprover
let get_transf_string s tr =
String.concat " " (Session_itp.get_transf_name s tr :: Session_itp.get_transf_args s tr)
let rec transf_depth s tr =
List.fold_left
......
......@@ -110,6 +110,9 @@ val get_used_provers_goal : Session_itp.session -> Session_itp.proofNodeID
(** [get_used_provers_goal s g] returns the set of provers used
somewhere under the goal [g] of session [s] *)
val get_transf_string : Session_itp.session -> Session_itp.transID -> string
(** [get_transf_string s tr] concatenates the name of transformation [tr]
in session [s] with its arguments *)
val goal_depth : Session_itp.session -> Session_itp.proofNodeID -> int
(** [goal_depth s g] returns the depth of the tree under goal
......
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