Finally made the editor preference setting working

ROADMAP

@@ -98,8 +98,8 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
 * Improved IDE:
  - left scrollbar + selection of shown or hidden provers
  - font enlargement
- - integration of support for prover upgrade
- - !!TODO!! support for selection of alternate editors
+ - integration of the support for prover upgrade
+ - support for selection of alternate editors
 * what else ?
 * see also the file CHANGES
 
@@ -136,14 +136,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
 == TODOs ==
 
 
-* (TOUS) Faire marcher la selection de l'editeur associé a un prouveur
-dans l'IDE
-** probleme: le choix n'est pas pris en compte, pas enregistré
-** question subsidaire: remise en cause du systeme de Whyconf inutilement
-   compliqué et tres difficile a maintenir.
-   La raison initiale "permettre a l'IDE de stocker sa config dans
-   le meme fichier .conf" ne me semble pas justifier une telle complication
-
 * DONE Document the Coq plugin and tactic
 ** DONE option timelimit <n>
 ** DONE renommer "coq-plugin" en "coq-tactic"

src/ide/gconfig.ml

@@ -41,10 +41,7 @@ type t =
       mutable window_height : int;
       mutable tree_width : int;
       mutable task_height : int;
-      mutable time_limit : int;
-      mutable mem_limit : int;
       mutable verbose : int;
-      mutable max_running_processes : int;
       mutable default_editor : string;
       mutable intro_premises : bool;
       mutable show_labels : bool;
@@ -182,7 +179,7 @@ let load_altern alterns (_,section) =
   Mprover.add unknown known alterns
 
 let load_config config original_config =
-  let main = get_main config in
+  (* let main = get_main config in *)
   let ide  = match get_section config "ide" with
     | None -> default_ide
     | Some s -> load_ide s
@@ -198,8 +195,6 @@ let load_config config original_config =
     window_width  = ide.ide_window_width;
     tree_width    = ide.ide_tree_width;
     task_height   = ide.ide_task_height;
-    time_limit    = Whyconf.timelimit main;
-    mem_limit     = Whyconf.memlimit main;
     verbose       = ide.ide_verbose;
     intro_premises= ide.ide_intro_premises ;
     show_labels   = ide.ide_show_labels ;
@@ -209,7 +204,6 @@ let load_config config original_config =
     premise_color = ide.ide_premise_color;
     goal_color = ide.ide_goal_color;
     error_color = ide.ide_error_color;
-    max_running_processes = Whyconf.running_provers_max main;
     default_editor = ide.ide_default_editor;
     config         = config;
     original_config = original_config;
@@ -238,14 +232,28 @@ let load_config config original_config =
 
   *)
 
+let debug_save_config n c =
+  let coq = { prover_name = "Coq" ; prover_version = "8.3pl3"; 
+              prover_altern = "" } in
+  let p = Mprover.find coq (get_provers c) in
+  let time = Whyconf.timelimit (Whyconf.get_main c) in
+  Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@." 
+    n time p.editor
+
 let save_config t =
+  eprintf "[Info] saving IDE config file@.";
+  (* taking original config, without the extra_config *)
   let config = t.original_config in
-  let config = set_main config
-    (set_limits (get_main config)
-       t.time_limit t.mem_limit t.max_running_processes)
-  in
-  (* let _,alterns = Mprover.fold save_altern t.altern_provers (0,[]) in *)
-  (* let config = set_family config "alternative_prover" alterns in *)
+  (* copy possibly modified settings to original config *)
+  let new_main = Whyconf.get_main t.config in
+  let time = Whyconf.timelimit new_main in
+  let mem = Whyconf.memlimit new_main in
+  let nb = Whyconf.running_provers_max new_main in
+  let config = set_main config (set_limits (get_main config) time mem nb) in
+  (* copy also provers section since it may have changed (the editor
+     can be set via the preferences dialog) *)
+  let config = set_provers config (get_provers t.config) in
+  (* copy also the possibly changed policies *)
   let config = set_policies config (get_policies t.config) in
   let ide = empty_section in
   let ide = set_int ide "window_height" t.window_height in
@@ -262,17 +270,9 @@ let save_config t =
   let ide = set_string ide "goal_color" t.goal_color in
   let ide = set_string ide "error_color" t.error_color in
   let ide = set_string ide "default_editor" t.default_editor in
-  (* let ide = set_string ~default:"ask" ide "replace_prover" *)
-  (*   (match t.replace_prover with *)
-  (*     | CRP_Ask -> "ask" *)
-  (*     | CRP_Not_Obsolete -> "never not obsolete")  in *)
   let ide = set_stringl ide "hidden_prover" t.hidden_provers in
   let config = set_section config "ide" ide in
-(* TODO: store newly detected provers !
-  let config = set_provers config
-    (Mstr.fold save_prover t.provers Mstr.empty) in
-*)
-  save_config config
+  Whyconf.save_config config
 
 let read_config conf_file extra_files =
   try
@@ -494,17 +494,21 @@ let general_settings c (notebook:GPack.notebook) =
   in
 *)
   (* timelimit ? *)
+  let main = Whyconf.get_main c.config in
+  let timelimit = ref (Whyconf.timelimit main) in
+  let memlimit = ref (Whyconf.memlimit main) in
   let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
   let _ = GMisc.label ~text:"Time limit: "
     ~packing:(hb#pack ~expand:false) () in
   let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
-  timelimit_spin#adjustment#set_value (float_of_int c.time_limit);
+  timelimit_spin#adjustment#set_value (float_of_int !timelimit);
   let (_ : GtkSignal.id) =
     timelimit_spin#connect#value_changed ~callback:
-      (fun () -> c.time_limit <- timelimit_spin#value_as_int)
+      (fun () -> timelimit := timelimit_spin#value_as_int)
   in
   (* nb of processes ? *)
+  let nb_processes = ref (Whyconf.running_provers_max main) in
   let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
   let _ = GMisc.label ~text:"Nb of processes: "
     ~packing:(hb#pack ~expand:false) () in
@@ -512,10 +516,10 @@ let general_settings c (notebook:GPack.notebook) =
   nb_processes_spin#adjustment#set_bounds
     ~lower:1. ~upper:16. ~step_incr:1. ();
   nb_processes_spin#adjustment#set_value
-    (float_of_int c.max_running_processes);
+    (float_of_int !nb_processes);
   let (_ : GtkSignal.id) =
     nb_processes_spin#connect#value_changed ~callback:
-      (fun () -> c.max_running_processes <- nb_processes_spin#value_as_int)
+      (fun () -> nb_processes := nb_processes_spin#value_as_int)
   in
   let display_options_frame =
     GBin.frame ~label:"Display options"
@@ -611,8 +615,7 @@ let general_settings c (notebook:GPack.notebook) =
   let _fillbox =
     GPack.vbox ~packing:(page#pack ~expand:true) ()
   in
-  ()
-
+  timelimit, memlimit, nb_processes
 
 (* Page "Provers" *)
 
@@ -742,8 +745,8 @@ let editors_page c (notebook:GPack.notebook) =
                 | "default" -> ""
                 | s -> s
             in
-	    Format.eprintf "prover %a : selected editor '%s'@."
-              print_prover p data;
+	    (* Format.eprintf "prover %a : selected editor '%s'@." *)
+            (*   print_prover p data; *)
             let provers = Whyconf.get_provers c.config in
             c.config <-
               Whyconf.set_provers c.config
@@ -764,7 +767,7 @@ let preferences (c : t) =
   let vbox = dialog#vbox in
   let notebook = GPack.notebook ~packing:vbox#add () in
   (** page "general settings" **)
-  general_settings c notebook;
+  let t,m,n = general_settings c notebook in
   (*** page "editors" **)
   editors_page c notebook;
   (** page "Provers" **)
@@ -788,7 +791,13 @@ let preferences (c : t) =
   (** bottom button **)
   dialog#add_button "Close" `CLOSE ;
   let ( _ : GWindow.Buttons.about) = dialog#run () in
-  eprintf "saving IDE config file@.";
+  (* let config = set_main config *)
+  (*   (set_limits (get_main config) *)
+  (*      t.time_limit t.mem_limit t.max_running_processes) *)
+  (* in *)
+
+  c.config <- Whyconf.set_main c.config
+    (Whyconf.set_limits (Whyconf.get_main c.config) !t !m !n);
   save_config ();
   dialog#destroy ()
 

src/ide/gconfig.mli

@@ -21,20 +21,12 @@
 open Why3
 open Whyconf
 
-(** Todo do something generic perhaps*)
-(* type conf_replace_prover = *)
-(*   | CRP_Ask *)
-(*   | CRP_Not_Obsolete *)
-
 type t =
     { mutable window_width : int;
       mutable window_height : int;
       mutable tree_width : int;
       mutable task_height : int;
-      mutable time_limit : int;
-      mutable mem_limit : int;
       mutable verbose : int;
-      mutable max_running_processes : int;
       mutable default_editor : string;
       mutable intro_premises : bool;
       mutable show_labels : bool;

src/ide/gmain.ml

@@ -414,7 +414,7 @@ let clear model = model#clear ()
 let image_of_result ~obsolete result =
   match result with
     | Session.Undone Session.Interrupted -> !image_undone
-    | Session.Undone Session.Unedited 
+    | Session.Undone Session.Unedited
     | Session.Undone Session.JustEdited -> !image_unknown
     | Session.Undone Session.Scheduled -> !image_scheduled
     | Session.Undone Session.Running -> !image_running
@@ -536,7 +536,7 @@ let update_task_view a =
     | S.Goal g ->
       if (Gconfig.config ()).intro_premises then
         let trans =
-          Trans.lookup_transform intro_transformation (env_session()).S.env 
+          Trans.lookup_transform intro_transformation (env_session()).S.env
         in
         display_task (Trans.apply trans (S.goal_task g))
       else
@@ -587,7 +587,7 @@ module M = Session_scheduler.Make
        session_needs_saving := true;
        let (_:bool) = goals_model#remove row#iter in ()
 
-     let reset () = 
+     let reset () =
        session_needs_saving := true;
        goals_model#clear ()
 
@@ -765,7 +765,9 @@ let sched =
       M.update_session ~allow_obsolete:true session gconfig.env
         gconfig.Gconfig.config
     in
-    let sched = M.init gconfig.max_running_processes in
+    let sched = M.init (Whyconf.running_provers_max
+                          (Whyconf.get_main gconfig.config))
+    in
     dprintf debug "@]@\n[Info] Opening session: done@.";
     session_needs_saving := false;
     current_env_session := Some env;
@@ -804,6 +806,7 @@ let () =
 (*****************************************************)
 
 let prover_on_selected_goals pr =
+  let timelimit = Whyconf.timelimit (Whyconf.get_main gconfig.config) in
   List.iter
     (fun row ->
       try
@@ -811,7 +814,7 @@ let prover_on_selected_goals pr =
        M.run_prover
          (env_session()) sched
          ~context_unproved_goals_only:!context_unproved_goals_only
-         ~timelimit:gconfig.time_limit
+         ~timelimit
          pr a
       with e ->
         eprintf "@[Exception raised while running a prover:@ %a@.@]"
@@ -938,18 +941,20 @@ let (_ : GMenu.image_menu_item) =
       begin
         match !current_env_session with
           | None -> ()
-          | Some _e ->
-            (* Can't do that since field .whyconf is not mutable *)
-            (* e.Session.whyconf <- gconfig.config *)
-            ()
+          | Some e ->
+              Session.update_env_session_config e gconfig.config;
+              Session.unload_provers e
       end;
       !refresh_provers ();
+(*
       Mprover.iter
         (fun p pi ->
           Format.eprintf "editor for %a : %s@." Whyconf.print_prover p
             pi.editor)
         (Whyconf.get_provers gconfig.config);
-      M.set_maximum_running_proofs gconfig.max_running_processes sched)
+*)
+      let nb = Whyconf.running_provers_max (Whyconf.get_main gconfig.config) in
+      M.set_maximum_running_proofs nb sched)
     ()
 
 let add_refresh_provers f _msg =
@@ -975,7 +980,6 @@ let save_session () =
 
 
 let exit_function ?(destroy=false) () =
-  eprintf "[Info] saving IDE config file@.";
   save_config ();
   if not !session_needs_saving then GMain.quit () else
   match (Gconfig.config ()).saving_policy with
@@ -1023,7 +1027,7 @@ let enlarge_font () =
   ()
 
 let reduce_font () =
-  decr font_size; 
+  decr font_size;
   change_font ();
 (*
   GConfig.save ()
@@ -1511,8 +1515,18 @@ let edit_selected_row r =
     | S.File _file ->
         ()
     | S.Proof_attempt a ->
-        M.edit_proof
-          (env_session()) sched ~default_editor:gconfig.default_editor a
+        let e = env_session () in
+(*
+        let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
+                    prover_altern = "" } in
+        let c = e.Session.whyconf in
+        let p = Mprover.find coq (get_provers c) in
+        let time = Whyconf.timelimit (Whyconf.get_main c) in
+        Format.eprintf
+          "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
+          0 time p.editor;
+*)
+        M.edit_proof e sched ~default_editor:gconfig.default_editor a
     | S.Transf _ -> ()
 
 let edit_current_proof () =
@@ -1695,7 +1709,7 @@ let () =
 (***************)
 
 
- 
+
 (* to be run when a row in the tree view is selected *)
 let select_row r =
   let ind = goals_model#get ~row:r#iter ~column:index_column in

src/session/session.ml

@@ -119,10 +119,11 @@ type loaded_provers = loaded_prover option PHprover.t
 
 type 'a env_session =
     { env : Env.env;
-      whyconf : Whyconf.config;
+      mutable whyconf : Whyconf.config;
       loaded_provers : loaded_provers;
       session : 'a session}
 
+let update_env_session_config e c = e.whyconf <- c
 
 (*************************)
 (**       Iterators      *)
@@ -1138,6 +1139,8 @@ let load_prover eS prover =
     PHprover.add eS.loaded_provers prover r;
     r
 
+let unload_provers eS = PHprover.clear eS.loaded_provers
+
 let () = Exn_printer.register
   (fun fmt exn ->
     match exn with

src/session/session.mli

@@ -173,13 +173,20 @@ type loaded_provers = loaded_prover option PHprover.t
 
 type 'a env_session = private
     { env : Env.env;
-      whyconf : Whyconf.config;
+      mutable whyconf : Whyconf.config;
       loaded_provers : loaded_provers;
       session : 'a session}
 
+val update_env_session_config : 'a env_session -> Whyconf.config -> unit
+(** updates the configuration *)
+
 val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
 (** load a prover *)
 
+val unload_provers : 'a env_session -> unit
+(** forces unloading of all provers, 
+    to force reading again the configuration *)
+
 (** {2 Update session} *)
 
 type 'key keygen = ?parent:'key -> unit -> 'key