Commit 94b94f59 authored by MARCHE Claude's avatar MARCHE Claude

uninstalled provers : dialog for setting policy activated (remaining issues below)

- the new policy is not taken into account immediately, only after
  saving preferences and restarting
- prover name is not dynamically changed in IDE, only in session (so
  visible after reloading only)
- dialog appear several times if several proof attempts launched
  in parallel
parent 7023491c
......@@ -928,3 +928,15 @@ let absolute_driver_file main s =
let load_driver main env file extras =
let file = absolute_driver_file main file in
Driver.load_driver_absolute env file extras
let unknown_to_known_provers provers pu =
Mprover.fold (fun pk _ (others,name,version) ->
match
pk.prover_name = pu.prover_name,
pk.prover_version = pu.prover_version,
pk.prover_altern = pu.prover_altern with
| false, _, _ -> pk::others, name, version
| _, false, _ -> others, pk::name, version
| _ -> others, name, pk::version
) provers ([],[],[])
......@@ -273,3 +273,8 @@ val load_driver : main -> Env.env -> string -> string list -> Driver.driver
(** wrapper for loading a driver from a file that may be relative to the datadir.
See [Driver.load_driver_absolute]
*)
val unknown_to_known_provers :
config_prover Mprover.t -> prover ->
prover list * prover list * prover list
(** return others, same name, same version *)
......@@ -1165,18 +1165,16 @@ let run_auto_detection gconfig =
(*let () = Debug.dprintf debug "[config] end of configuration initialization@."*)
(*
let uninstalled_prover c eS unknown =
try
Whyconf.get_prover_upgrade_policy c.config unknown
with Not_found ->
let others,names,versions = Session_tools.unknown_to_known_provers
(Whyconf.get_provers eS.Session.whyconf) unknown in
let dialog = GWindow.dialog
~icon:(!why_icon) ~modal:true
~title:"Why3: Uninstalled prover" ()
in
let vbox = dialog#vbox in
let uninstalled_prover_dialog c unknown =
let others,names,versions =
Whyconf.unknown_to_known_provers
(Whyconf.get_provers c.config) unknown
in
let dialog = GWindow.dialog
~icon:(!why_icon) ~modal:true
~title:"Why3: Uninstalled prover" ()
in
let vbox = dialog#vbox in
(* Does not work: why ??
let vbox_pack = vbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
let hbox = GPack.hbox ~packing:vbox_pack () in
......@@ -1274,8 +1272,7 @@ let uninstalled_prover c eS unknown =
| _ -> assert false
in
c.config <- set_prover_upgrade_policy c.config unknown policy;
policy
*)
()
(*
......
......@@ -116,10 +116,9 @@ val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
(*
val uninstalled_prover :
t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
*)
val uninstalled_prover_dialog :
t -> Whyconf.prover -> unit
(*
val unknown_prover :
......
......@@ -1907,7 +1907,11 @@ let treat_notification n =
| Proof_status_change (pa, obs, l) ->
let r = get_node_row id in
Hint.replace node_id_pa id (pa, obs, l);
set_status_and_time_column ~limit:l r
set_status_and_time_column ~limit:l r;
match pa with
| Controller_itp.Uninstalled p ->
uninstalled_prover_dialog gconfig p
| _ -> ()
end
| Next_Unproven_Node_Id (asked_id, next_unproved_id) ->
if_selected_alone asked_id
......
......@@ -404,7 +404,7 @@ let interp commands_table cont id s =
pa.Session_itp.prover in
Edit p
with Not_found ->
QError "prover not found"
QError "cannot edit: uninstalled prover"
end
| _ -> QError ("Please select a proof node in the task tree")
end
......
......@@ -102,17 +102,6 @@ type to_prover =
| To_prover of prover
| SameProver
let unknown_to_known_provers provers pu =
Mprover.fold (fun pk _ (others,name,version) ->
match
pk.prover_name = pu.prover_name,
pk.prover_version = pu.prover_version,
pk.prover_altern = pu.prover_altern with
| false, _, _ -> pk::others, name, version
| _, false, _ -> others, pk::name, version
| _ -> others, name, pk::version
) provers ([],[],[])
let get_to_prover pk session config =
match pk with
| Some pk -> To_prover pk
......
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