ide: provers with full names

src/ide/why3ide.ml

@@ -1505,7 +1505,7 @@ let provers_factory =
   let tools_submenu_provers = tools_factory#add_submenu "Provers" in
   new GMenu.factory tools_submenu_provers
 
-let add_submenu_prover prover =
+let add_submenu_prover (shortcut,prover) =
 (*
   let provers =
     C.Mprover.fold
@@ -1519,16 +1519,16 @@ let add_submenu_prover prover =
   C.Mprover.iter
     (fun p _ ->
  *)
-  let n = (*Pp.string_of_wnl Whyconf.print_prover *) prover in
-  let (_ : GMenu.image_menu_item) =
-    provers_factory#add_image_item ~label:n
-                                   ~callback:(fun () ->
-                                              Debug.dprintf debug "[IDE INFO] interp command '%s'@." n;
-                                              interp n;
-                                              (* send_request (Command_req (id, n)) *)
-)
-                                   ()
+  let  i = create_menu_item
+             provers_factory
+             prover
+             ("run prover " ^ prover ^ " on selected goal (shortcut: " ^ shortcut ^ ")")
   in
+  let callback () =
+    Debug.dprintf debug "[IDE INFO] interp command '%s'@." shortcut;
+    interp shortcut
+  in
+  connect_menu_item i ~callback
 (* prover button, obsolete
   let b = GButton.button ~packing:provers_box#add ~label:n () in
   b#misc#set_tooltip_markup
@@ -1539,7 +1539,6 @@ let add_submenu_prover prover =
       ~callback:(fun () -> prover_on_selected_goals p)
   in
  *)
-  ()
 
 
 let init_completion provers transformations commands =
@@ -1550,8 +1549,16 @@ let init_completion provers transformations commands =
   (* todo: add queries *)
 
   (* add provers *)
-  List.iter add_completion_entry provers;
-  List.iter add_submenu_prover provers;
+  let all_strings =
+    List.fold_left (fun acc (s,p) ->  s :: p :: acc) [] provers
+  in
+  List.iter add_completion_entry all_strings;
+  let provers_sorted =
+    List.sort (fun (_,p1) (_,p2) ->
+               String.compare (Strings.lowercase p1) (Strings.lowercase p2))
+              provers
+  in
+  List.iter add_submenu_prover provers_sorted;
 
   add_completion_entry "auto";
   add_completion_entry "auto 2";

src/session/itp_communication.ml

@@ -10,7 +10,7 @@ let root_node : node_ID = 0
 
 type global_information =
     {
-     provers         : prover list;
+     provers         : (string * prover) list;
      transformations : transformation list;
      strategies      : strategy list;
      commands        : string list;

src/session/itp_communication.mli

@@ -11,7 +11,7 @@ val root_node : node_ID
    shared with the IDE through communication *)
 type global_information =
     {
-     provers         : prover list;
+     provers         : (string * prover) list;
      transformations : transformation list;
      strategies      : strategy list;
      commands        : string list

src/session/itp_server.ml

@@ -630,8 +630,6 @@ end
       Format.eprintf "Fatal error while loading itp driver: %a@." Exn_printer.exn_printer e;
       exit 1
 
-  let get_prover_list (config: Whyconf.config) =
-    Mstr.fold (fun x _ acc -> x :: acc) (Whyconf.get_prover_shortcuts config) []
 
   (* -----------------------------------   ------------------------------------- *)
 
@@ -895,7 +893,11 @@ end
                      { task_driver = task_driver;
                        cont = c };
     let d = get_server_data () in
-    let prover_list = get_prover_list config in
+    let prover_list =
+      Mstr.fold (fun x p acc ->
+                 let n = Pp.sprintf "%a" Whyconf.print_prover p in
+                 (x,n) :: acc) (Whyconf.get_prover_shortcuts config) []
+    in
     let transformation_list = List.map fst (list_transforms ()) in
     let strategies_list =
       let l = strategies d.cont.controller_env config loaded_strategies in

src/session/json_util.ml

@@ -12,8 +12,12 @@ let convert_prover_to_json (p: Whyconf.prover) =
      "prover_altern", String p.Whyconf.prover_altern])
 
 let convert_infos (i: global_information) =
+  let convert_prover (s,p) =
+    Record (convert_record ["prover_shorcut", String s;
+                            "prover_name", String p])
+  in
   Record (convert_record
-    ["provers", List (List.map (fun x -> String x) i.provers);
+    ["provers", List (List.map convert_prover i.provers);
      "transformations", List (List.map (fun x -> String x) i.transformations);
      "strategies", List (List.map (fun x -> String x) i.strategies);
      "commands", List (List.map (fun x -> String x) i.commands)])
@@ -617,7 +621,10 @@ let parse_infos j =
     let tr = get_list (get_field j "transformations") in
     let str = get_list (get_field j "strategies") in
     let com = get_list (get_field j "commands") in
-    {provers = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) pr;
+    {provers = List.map (fun j -> try
+                                 (get_string (get_field j "prover_shortcut"),
+                                  get_string (get_field j "prover_name"))
+                               with Not_found -> raise NotInfos) pr;
      transformations = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) tr;
      strategies = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) str;
      commands = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) com}