Commit af8c5211 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add (none) as the first prover entry.

Otherwise the default prover might be incorrectly shown to the user. For
example, if the user never set a default prover, the interface shows that
Alt-Ergo (or whatever comes first) is the default prover, while nothing
happens when pressing 'p'.
parent b96759cc
...@@ -890,16 +890,20 @@ let provers_page c (notebook:GPack.notebook) = ...@@ -890,16 +890,20 @@ let provers_page c (notebook:GPack.notebook) =
let provers_box = let provers_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5 GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:frame2#add () in ~packing:frame2#add () in
let group = ref None in let group =
let b =
GButton.radio_button ~label:"(none)" ~packing:provers_box#add
~active:(c.default_prover = "") () in
let (_ : GtkSignal.id) =
b#connect#toggled ~callback:(fun () -> c.default_prover <- "") in
b#group in
Mprover.iter Mprover.iter
(fun _ p -> (fun _ p ->
let name = prover_parseable_format p.prover in let name = prover_parseable_format p.prover in
let label = Pp.string_of_wnl print_prover p.prover in let label = Pp.string_of_wnl print_prover p.prover in
let b = let b =
GButton.radio_button ~label ?group:!group ~packing:provers_box#add () GButton.radio_button ~label ~group ~packing:provers_box#add
~active:(name = c.default_prover) ~active:(name = c.default_prover) () in
in
if !group = None then group := Some b#group;
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
b#connect#toggled ~callback:(fun () -> c.default_prover <- name) b#connect#toggled ~callback:(fun () -> c.default_prover <- name)
in ()) 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