Commit abb66e65 authored by François Bobot's avatar François Bobot

Fix : take into account all the prover fields not only name or version

parent ba1da570
......@@ -93,7 +93,7 @@ type prover =
val print_prover : Format.formatter -> prover -> unit
(** Printer for prover *)
module Prover : Util.OrderedHash with type t = prover
module Mprover : Stdlib.Map.S with type key = prover
module Sprover : Mprover.Set
module Hprover : Hashtbl.S with type key = prover
......
......@@ -545,7 +545,7 @@ let init =
| S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a ->
let p = a.S.proof_prover in
p.C.prover_name ^ " " ^ p.C.prover_version
Pp.string_of_wnl C.print_prover p
| S.Transf tr -> tr.S.transf_name);
notify any
......@@ -997,15 +997,16 @@ let () =
let add_item_provers () =
C.Mprover.iter
(fun p _ ->
let n = p.C.prover_name ^ " " ^ p.C.prover_version in
let n = Pp.string_of_wnl C.print_prover p in
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item ~label:n
~callback:(fun () -> prover_on_selected_goals p)
()
in
let b = GButton.button ~packing:provers_box#add ~label:n () in
b#misc#set_tooltip_markup ("Start <tt>" ^ p.C.prover_name ^
"</tt> on the <b>selected goals</b>");
b#misc#set_tooltip_markup
(Pp.sprintf_wnl "Start <tt>%a</tt> on the <b>selected goals</b>"
C.print_prover p);
(* prend de la place pour rien
let i = GMisc.image ~pixbuf:(!image_prover) () in
......
......@@ -153,7 +153,7 @@ let run_file (context : context) print_session f =
module Simple =
struct
let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
let print_prover = Whyconf.print_prover
let print_proof_status fmt = function
| Undone _ -> fprintf fmt "Undone"
......@@ -223,7 +223,7 @@ struct
then fprintf fmt "class='verified'"
else fprintf fmt "class='notverified'"
let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
let print_prover = Whyconf.print_prover
let print_proof_status fmt = function
| Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
......
......@@ -173,11 +173,11 @@ let init =
(*
let cpt = ref 0 in
*)
fun _row any ->
fun _row _any ->
(*
incr cpt;
Hashtbl.add model_index !cpt any;
*)
let _name =
match any with
| S.Goal g -> S.goal_expl g
......@@ -188,6 +188,7 @@ let init =
p.C.prover_name ^ " " ^ p.C.prover_version
| S.Transf tr -> tr.S.transf_name
in
*)
(* eprintf "Item '%s' loaded@." name *)
()
......@@ -344,8 +345,6 @@ let rec provers_latex_stats provers theory =
S.theory_iter_proof_attempt (fun a ->
Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
let prover_name a = a.C.prover_name ^ " " ^ a.C.prover_version
let protect s =
let b = Buffer.create 7 in
for i = 0 to String.length s - 1 do
......@@ -503,7 +502,7 @@ let print_head n depth provers fmt =
(depth + 1)
else
fprintf fmt "\\hline Proof obligations ";
List.iter (fun a -> fprintf fmt "& \\provername{%s} " a.C.prover_name)
List.iter (fun a -> fprintf fmt "& \\provername{%a} " C.print_prover a)
provers;
fprintf fmt "\\\\ @."
......@@ -553,9 +552,7 @@ let theory_latex_stat n table dir t =
provers_latex_stats provers t;
let provers = Hashtbl.fold (fun _ pr acc -> pr :: acc)
provers [] in
let provers =
List.sort (fun p1 p2 -> String.compare p1.C.prover_name p2.C.prover_name)
provers in
let provers = List.sort C.Prover.compare provers in
let depth = theory_depth t in
let name = t.S.theory_name.Ident.id_string in
let ch = open_out (Filename.concat dir(name^".tex")) in
......
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