Adding transformation doc in the completion. (first attempt)

src/ide/why3ide.ml

@@ -1934,7 +1934,7 @@ let add_submenu_prover (shortcut,prover_name,prover_parseable_name) =
 
 let init_completion provers transformations strategies commands =
   (* add the names of all the the transformations *)
-  List.iter (fun s -> add_completion_entry (s,"transformation")) transformations;
+  List.iter add_completion_entry transformations;
   (* add the name of the commands *)
   List.iter (fun s -> add_completion_entry (s,"command")) commands;
   (* todo: add queries *)

src/session/itp_communication.ml

@@ -11,7 +11,7 @@
 
 (* Information that the IDE may want to have *)
 type prover = string
-type transformation = string
+type transformation = (string * string)
 type strategy = string
 
 

src/session/itp_communication.mli

@@ -10,7 +10,8 @@
 (********************************************************************)
 
 type prover = string
-type transformation = string
+(* Name and description *)
+type transformation = (string * string)
 type strategy = string
 
 type node_ID = int

src/session/itp_server.ml

@@ -1042,7 +1042,7 @@ end
          (s,n,p) :: acc) (Whyconf.get_provers config) []
     in
     load_strategies c;
-    let transformation_list = List.map fst (list_transforms ()) in
+    let transformation_list = List.map (fun (a, b) -> (a, Format.sprintf "%( %)" b)) (list_transforms ()) in
     let strategies_list = list_strategies c in
     let infos =
       {

src/session/json_util.ml

@@ -34,7 +34,11 @@ let convert_infos (i: global_information) =
   in
   Record (convert_record
     ["provers", List (List.map convert_prover i.provers);
-     "transformations", List (List.map (fun x -> String x) i.transformations);
+     "transformations",
+     List (List.map
+             (fun (a, b) ->
+               Record (convert_record ["name_t", String a; "desc_t", String b]))
+             i.transformations);
      "strategies", List (List.map convert_strategy i.strategies);
      "commands", List (List.map (fun x -> String x) i.commands)])
 
@@ -567,6 +571,12 @@ let parse_infos j =
   try
     let pr = get_list (get_field j "provers") in
     let tr = get_list (get_field j "transformations") in
+    let tr =
+      List.map (fun j ->
+        try
+          get_string (get_field j "name_t"),
+          get_string (get_field j "desc_t")
+        with | _ -> raise (NotInfos "transformations")) tr in
     let str = get_list (get_field j "strategies") in
     let com = get_list (get_field j "commands") in
     {provers = List.map (fun j -> try
@@ -574,7 +584,7 @@ let parse_infos j =
                                   get_string (get_field j "prover_name"),
                                   get_string (get_field j "prover_parseable_name"))
                                with Not_found -> raise (NotInfos "provers")) pr;
-     transformations = List.map (fun j -> match j with | String x -> x | _ -> raise (NotInfos "transformations")) tr;
+     transformations = tr;
      strategies = List.map (fun j -> try
                                  (get_string (get_field j "strategy_shortcut"),
                                   get_string (get_field j "strategy_name"))