Commit 8863d225 authored by Andrei Paskevich's avatar Andrei Paskevich

IDE: stock hidden provers in why3.conf with correct names

parent 48ba3b6d
......@@ -61,10 +61,12 @@ let print_prover fmt p =
p.prover_name p.prover_version
(if p.prover_altern = "" then "" else " ") p.prover_altern
let print_prover_parsable_format fmt p =
Format.fprintf fmt "%s,%s,%s"
let prover_parseable_format p =
Format.sprintf "%s,%s,%s"
p.prover_name p.prover_version p.prover_altern
let print_prover_parseable_format fmt p =
Format.pp_print_string fmt (prover_parseable_format p)
module Prover = struct
type t = prover
......
......@@ -95,7 +95,8 @@ type prover =
(** record of necessary data for a given external prover *)
val print_prover : Format.formatter -> prover -> unit
val print_prover_parsable_format : Format.formatter -> prover -> unit
val print_prover_parseable_format : Format.formatter -> prover -> unit
val prover_parseable_format : prover -> string
(** Printer for prover *)
module Prover : OrderedHashedType with type t = prover
......
......@@ -774,10 +774,10 @@ let provers_page c (notebook:GPack.notebook) =
let hidden_provers = Hashtbl.create 7 in
Mprover.iter
(fun _ p ->
let p = p.prover in
let label = p.prover_name ^ " " ^ p.prover_version in
let hidden = ref (List.mem label c.hidden_provers) in
Hashtbl.add hidden_provers label hidden;
let name = prover_parseable_format p.prover in
let label = Pp.string_of_wnl print_prover p.prover in
let hidden = ref (List.mem name c.hidden_provers) in
Hashtbl.add hidden_provers name hidden;
let b =
GButton.check_button ~label ~packing:provers_box#add ()
~active:(not !hidden)
......@@ -863,7 +863,7 @@ let editors_page c (notebook:GPack.notebook) =
in
let strings = "(default)" :: "--" :: (List.rev strings) in
let add_prover p pi =
let text = p.prover_name ^ " " ^ p.prover_version in
let text = Pp.string_of_wnl Whyconf.print_prover p in
let hb = GPack.hbox ~homogeneous:false ~packing:box#pack () in
let _ = GMisc.label ~width:150 ~xalign:0.0 ~text ~packing:(hb#pack ~expand:false) () in
let (combo, ((_ : GTree.list_store), column)) =
......
......@@ -1405,8 +1405,7 @@ let () =
C.Mprover.fold
(fun k p acc ->
let pr = p.prover in
if List.mem (pr.prover_name ^ " " ^ pr.prover_version)
gconfig.hidden_provers
if List.mem (C.prover_parseable_format pr) gconfig.hidden_provers
then acc
else C.Mprover.add k p acc)
provers C.Mprover.empty
......
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