make all provers visible both in tools menu and in completion

src/driver/whyconf.ml

@@ -58,10 +58,12 @@ type prover =
       prover_altern : string;
     }
 
+let print_altern fmt s =
+  if s <> "" then Format.fprintf fmt " (%s)" s
+
 let print_prover fmt p =
-  Format.fprintf fmt "%s (%s%s%s)"
-    p.prover_name p.prover_version
-    (if p.prover_altern = "" then "" else " ") p.prover_altern
+  Format.fprintf fmt "%s %s%a"
+    p.prover_name p.prover_version print_altern p.prover_altern
 
 let prover_parseable_format p =
   Format.sprintf "%s,%s,%s"

src/ide/why3ide.ml

@@ -903,7 +903,7 @@ let add_completion_entry s =
 let match_function s iter =
   let candidate = completion_model#get ~row:iter ~column:completion_col in
   try
-    ignore (Str.search_forward (Str.regexp s) candidate 0);
+    ignore (Str.search_forward (Str.regexp_string_case_fold s) candidate 0);
     true
   with Not_found -> false
 
@@ -1533,12 +1533,13 @@ let string_of_desc desc =
   in Glib.Markup.escape_text (Pp.string_of print_trans_desc desc)
 
 
+let pr_shortcut s = if s = "" then "" else "(shortcut: " ^ s ^ ")"
 
 let add_submenu_strategy (shortcut,strategy) =
   let  i = create_menu_item
              strategies_factory
              strategy
-             ("run strategy " ^ strategy ^ " on selected goal (shortcut: " ^ shortcut ^ ")")
+             ("run strategy " ^ strategy ^ " on selected goal" ^ pr_shortcut shortcut)
   in
   let callback () =
     Debug.dprintf debug "[IDE INFO] interp command '%s'@." shortcut;
@@ -1546,11 +1547,11 @@ let add_submenu_strategy (shortcut,strategy) =
   in
   connect_menu_item i ~callback
 
-let add_submenu_prover (shortcut,prover) =
+let add_submenu_prover (shortcut,prover,_) =
   let  i = create_menu_item
              provers_factory
              prover
-             ("run prover " ^ prover ^ " on selected goal (shortcut: " ^ shortcut ^ ")")
+             ("run prover " ^ prover ^ " on selected goal" ^ pr_shortcut shortcut)
   in
   let callback () =
     Debug.dprintf debug "[IDE INFO] interp command '%s'@." shortcut;
@@ -1568,13 +1569,16 @@ let init_completion provers transformations strategies commands =
   (* todo: add queries *)
 
   (* add provers *)
+
   let all_strings =
-    List.fold_left (fun acc (s,p) ->  s :: p :: acc) [] provers
+    List.fold_left (fun acc (s,_,p) ->
+                    Debug.dprintf debug "string for completion: '%s' '%s'@." s p;
+                    if s = "" then p :: acc else 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))
+    List.sort (fun (_,h1,_) (_,h2,_) ->
+               String.compare (Strings.lowercase h1) (Strings.lowercase h2))
               provers
   in
   List.iter add_submenu_prover provers_sorted;

src/session/itp_communication.ml

@@ -20,18 +20,19 @@ let root_node : node_ID = 0
 
 
 type global_information =
-    {
-     provers         : (string * prover) list;
-     transformations : transformation list;
-     strategies      : (string * strategy) list;
-     commands        : string list;
-     (* hidden_provers       : string list; *)
-     (* session_time_limit   : int; *)
-     (* session_mem_limit    : int; *)
+  {
+    provers         : (string * string * string) list;
+    (* (shortcut, human readable name, parseable name) *)
+    transformations : transformation list;
+    strategies      : (string * strategy) list;
+    commands        : string list;
+    (* hidden_provers       : string list; *)
+    (* session_time_limit   : int; *)
+    (* session_mem_limit    : int; *)
      (* session_nb_processes : int; *)
-     (* session_cntexample   : bool; *)
-     (* main_dir             : string *)
-    }
+    (* session_cntexample   : bool; *)
+    (* main_dir             : string *)
+  }
 
 type message_notification =
   | Proof_error           of node_ID * string

src/session/itp_communication.mli

@@ -21,18 +21,19 @@ val root_node : node_ID
 (** Global information known when server process has started and that can be
    shared with the IDE through communication *)
 type global_information =
-    {
-     provers         : (string * prover) list;
-     transformations : transformation list;
-     strategies      : (string * strategy) list;
-     commands        : string list
-     (* hidden_provers       : string list; *)
-     (* session_time_limit   : int; *)
-     (* session_mem_limit    : int; *)
-     (* session_nb_processes : int; *)
-     (* session_cntexample   : bool; *)
-     (* main_dir             : string *)
-    }
+  {
+    provers         : (string * string * string) list;
+    (* (shortcut, human readable name, parseable name) *)
+    transformations : transformation list;
+    strategies      : (string * strategy) list;
+    commands        : string list
+                             (* hidden_provers       : string list; *)
+                             (* session_time_limit   : int; *)
+                             (* session_mem_limit    : int; *)
+                             (* session_nb_processes : int; *)
+                             (* session_cntexample   : bool; *)
+                             (* main_dir             : string *)
+  }
 
 type message_notification =
   | Proof_error           of node_ID * string

src/session/itp_server.ml

@@ -971,10 +971,21 @@ end
                        send_source = send_source;
                      };
     let d = get_server_data () in
+    let shortcuts =
+      Mstr.fold
+        (fun s p acc -> Whyconf.Mprover.add p s acc)
+        (Whyconf.get_prover_shortcuts config) Whyconf.Mprover.empty
+    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) []
+      Whyconf.Mprover.fold
+        (fun pr _ acc ->
+         let s = try
+             Whyconf.Mprover.find pr shortcuts
+           with Not_found -> ""
+         in
+         let n = Pp.sprintf "%a" Whyconf.print_prover pr in
+         let p = Pp.sprintf "%a" Whyconf.print_prover_parseable_format pr in
+         (s,n,p) :: acc) (Whyconf.get_provers config) []
     in
     load_strategies c;
     let transformation_list = List.map fst (list_transforms ()) in

src/session/json_util.ml

@@ -23,9 +23,10 @@ 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) =
+  let convert_prover (s,h,p) =
     Record (convert_record ["prover_shorcut", String s;
-                            "prover_name", String p])
+                            "prover_name", String h;
+                            "prover_parseable_name", String p])
   in
   let convert_strategy (s,p) =
     Record (convert_record ["strategy_shorcut", String s;
@@ -589,7 +590,8 @@ let parse_infos j =
     let com = get_list (get_field j "commands") in
     {provers = List.map (fun j -> try
                                  (get_string (get_field j "prover_shortcut"),
-                                  get_string (get_field j "prover_name"))
+                                  get_string (get_field j "prover_name"),
+                                  get_string (get_field j "prover_parseable_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 -> try