time and mem limit temporary for session

src/ide/gconfig.ml

@@ -63,6 +63,9 @@ type t =
       (* mutable replace_prover : conf_replace_prover; *)
       (* hidden prover buttons *)
       mutable hidden_provers : string list;
+      mutable session_time_limit : int;
+      mutable session_mem_limit : int;
+      mutable session_nb_processes : int;
     }
 
 
@@ -189,7 +192,7 @@ let load_altern alterns (_,section) =
 *)
 
 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
@@ -222,7 +225,10 @@ let load_config config original_config =
     (* altern_provers = alterns; *)
     (* replace_prover = ide.ide_replace_prover; *)
     hidden_provers = ide.ide_hidden_provers;
-  }
+    session_time_limit = Whyconf.timelimit main;
+    session_mem_limit = Whyconf.memlimit main;
+    session_nb_processes = Whyconf.running_provers_max main;
+}
 
 
 (*
@@ -562,7 +568,7 @@ let show_about_window () =
 
 (**** Preferences Window ***)
 
-let general_settings c (notebook:GPack.notebook) =
+let general_settings (c : t) (notebook:GPack.notebook) =
   let label = GMisc.label ~text:"General" () in
   let page =
     GPack.vbox ~homogeneous:false ~packing:
@@ -579,45 +585,63 @@ let general_settings c (notebook:GPack.notebook) =
       (fun () -> c.verbose <- 1 - c.verbose)
   in
 *)
+  let external_processes_options_frame =
+    GBin.frame ~label:"External provers options"
+      ~packing:page#pack ()
+  in
+  let vb = GPack.vbox ~homogeneous:false
+    ~packing:external_processes_options_frame#add ()
+  in
   (* time limit *)
-  let main = Whyconf.get_main c.config in
   let width = 200 and xalign = 0.0 in
-  let timelimit = ref (Whyconf.timelimit main) in
-  let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
+  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
+  in
   let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
     ~packing:(hb#pack ~expand:false) () in
   let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:300. ~step_incr:1. ();
-  timelimit_spin#adjustment#set_value (float_of_int !timelimit);
+  timelimit_spin#adjustment#set_value (float_of_int c.session_time_limit);
   let (_ : GtkSignal.id) =
     timelimit_spin#connect#value_changed ~callback:
-      (fun () -> timelimit := timelimit_spin#value_as_int)
+      (fun () -> c.session_time_limit <- timelimit_spin#value_as_int)
   in
   (* mem limit *)
-  let memlimit = ref (Whyconf.memlimit main) in
-  let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
+  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
+  in
   let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
     ~packing:(hb#pack ~expand:false) () in
   let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:4000. ~step_incr:100. ();
-  memlimit_spin#adjustment#set_value (float_of_int !memlimit);
+  memlimit_spin#adjustment#set_value (float_of_int c.session_mem_limit);
   let (_ : GtkSignal.id) =
     memlimit_spin#connect#value_changed ~callback:
-      (fun () -> memlimit := memlimit_spin#value_as_int)
+      (fun () -> c.session_mem_limit <- memlimit_spin#value_as_int)
+  in
+  (* nb of processes *)
+  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
   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: " ~width ~xalign
     ~packing:(hb#pack ~expand:false) () in
   let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   nb_processes_spin#adjustment#set_bounds
     ~lower:1. ~upper:16. ~step_incr:1. ();
   nb_processes_spin#adjustment#set_value
-    (float_of_int !nb_processes);
+    (float_of_int c.session_nb_processes);
   let (_ : GtkSignal.id) =
     nb_processes_spin#connect#value_changed ~callback:
-      (fun () -> nb_processes := nb_processes_spin#value_as_int)
+      (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
+  in
+  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
+  let save_for_future = ref false in
+  let save =
+    GButton.check_button
+      ~label:"save settings above for future sessions"
+      ~packing:hb#add ()
+      ~active:false
+  in
+  let (_ : GtkSignal.id) =
+    save#connect#toggled ~callback:
+      (fun () -> save_for_future := not !save_for_future)
   in
   let display_options_frame =
     GBin.frame ~label:"Display options"
@@ -710,10 +734,10 @@ let general_settings c (notebook:GPack.notebook) =
   let (_ : GtkSignal.id) =
     choice2#connect#toggled ~callback:(set_saving_policy 2)
   in
-  let _fillbox =
+  let (_ : GPack.box) =
     GPack.vbox ~packing:(page#pack ~expand:true) ()
   in
-  timelimit, memlimit, nb_processes
+  save_for_future
 
 (* Page "Provers" *)
 
@@ -872,7 +896,7 @@ let preferences (c : t) =
   let vbox = dialog#vbox in
   let notebook = GPack.notebook ~packing:vbox#add () in
   (** page "general settings" **)
-  let t,m,n = general_settings c notebook in
+  let save_for_future_session = general_settings c notebook in
   (*** page "editors" **)
   editors_page c notebook;
   (** page "Provers" **)
@@ -901,8 +925,10 @@ let preferences (c : t) =
   (*      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);
+  if !save_for_future_session then
+    c.config <- Whyconf.set_main c.config
+      (Whyconf.set_limits (Whyconf.get_main c.config)
+         c.session_time_limit c.session_mem_limit c.session_nb_processes);
   save_config ();
   dialog#destroy ()
 

src/ide/gconfig.mli

@@ -43,6 +43,9 @@ type t =
       (* mutable altern_provers : prover option Mprover.t; *)
       (* mutable replace_prover : conf_replace_prover; *)
       mutable hidden_provers : string list;
+      mutable session_time_limit : int;
+      mutable session_mem_limit : int;
+      mutable session_nb_processes : int;
     }
 
 val read_config : string option -> string list -> unit

src/ide/gmain.ml

@@ -843,8 +843,7 @@ let sched =
         gconfig.Gconfig.config
     in
     Debug.dprintf debug "@]@\n[Info] Opening session: update done@.  @[<hov 2>";
-    let sched = M.init (Whyconf.running_provers_max
-                          (Whyconf.get_main gconfig.config))
+    let sched = M.init (gconfig.session_nb_processes)
     in
     Debug.dprintf debug "@]@\n[Info] Opening session: done@.";
     session_needs_saving := false;
@@ -881,9 +880,8 @@ let () =
 (*****************************************************)
 
 let prover_on_selected_goals pr =
-  let main = Whyconf.get_main gconfig.config in
-  let timelimit = Whyconf.timelimit main in
-  let memlimit = Whyconf.memlimit main in
+  let timelimit = gconfig.session_time_limit in
+  let memlimit = gconfig.session_mem_limit in
   List.iter
     (fun row ->
       try
@@ -1178,7 +1176,7 @@ let (_ : GMenu.image_menu_item) =
             pi.editor)
         (Whyconf.get_provers gconfig.config);
 *)
-      let nb = Whyconf.running_provers_max (Whyconf.get_main gconfig.config) in
+      let nb = gconfig.session_nb_processes in
       M.set_maximum_running_proofs nb sched)
     ()
 

src/printer/coq.ml

@@ -121,7 +121,9 @@ type info = {
   realization : bool;
 }
 
+(* unused printing function
 let print_path = print_list (constant_string ".") string
+*)
 
 let print_id fmt id = string fmt (id_unique iprinter id)
 
@@ -133,7 +135,9 @@ let print_id_real info fmt id =
 
 let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
 let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
+(* unused printing function
 let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
+*)
 
 (** Types *)
 
@@ -179,10 +183,14 @@ let unambig_fs fs =
 
 (** Patterns, terms, and formulas *)
 
+(* unused
 let lparen_l fmt () = fprintf fmt "@ ("
+*)
 let lparen_r fmt () = fprintf fmt "(@,"
+(* unused
 let print_paren_l fmt x =
   print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
+*)
 let print_paren_r fmt x =
   print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x
 
@@ -219,7 +227,9 @@ let print_binop fmt = function
   | Timplies -> fprintf fmt "->"
   | Tiff -> fprintf fmt "<->"
 
+(* unused
 let print_label fmt (l,_) = fprintf fmt "(*%s*)" l
+*)
 
 let protect_on x s = if x then "(" ^^ s ^^ ")" else s
 
@@ -227,7 +237,9 @@ let rec print_term info fmt t = print_lrterm false false info fmt t
 and     print_fmla info fmt f = print_lrfmla false false info fmt f
 and print_opl_term info fmt t = print_lrterm true  false info fmt t
 and print_opl_fmla info fmt f = print_lrfmla true  false info fmt f
+(* unused
 and print_opr_term info fmt t = print_lrterm false true  info fmt t
+*)
 and print_opr_fmla info fmt f = print_lrfmla false true  info fmt f
 
 and print_lrterm opl opr info fmt t = match t.t_label with