Configurable policy for saving session: Always/Never/Ask

ROADMAP

@@ -63,10 +63,6 @@
 * deplacer le bouton "Cancel" dans le menu "tools",
   le renommer en "make obsolete" et le documenter (A)
 
-* Rendre optionnel la question "would you like to save the session ?"
-   (C) -> 3-state options (Yes/No/ask) dans la config
-  + DONE dans le menu "file" : "save session" sans raccourci clavier
-
 * documenter les options de Why (A)
 
 * Distribution of examples: we should distribute those who have an xml file
@@ -78,7 +74,12 @@
 
 * distribute bench files (A + F)
 
+* DONE Rendre optionnel la question "would you like to save the session ?"
+   (C) -> 3-state options (Yes/No/ask) dans la config
+  + DONE dans le menu "file" : "save session" sans raccourci clavier
+
 * DONE desactiver "Save" (et editable=false dans la fenetre)
+
 * DONE mettre "Quit" en dernier (C)
 
 * DONE checkout frais, compilation (local ou non) et make bench chaque nuit sur moloch

src/ide/gconfig.ml

@@ -42,6 +42,8 @@ type t =
 *)
       mutable default_editor : string;
       mutable show_labels : bool;
+      mutable saving_policy : int;
+        (** 0 = always, 1 = never, 2 = ask *)
       mutable env : Env.env;
       mutable config : Whyconf.config;
     }
@@ -53,6 +55,7 @@ type ide = {
   ide_tree_width : int;
   ide_task_height : int;
   ide_verbose : int;
+  ide_saving_policy : int;
   ide_default_editor : string;
 }
 
@@ -62,6 +65,7 @@ let default_ide =
     ide_tree_width = 512;
     ide_task_height = 384;
     ide_verbose = 0;
+    ide_saving_policy = 0;
     ide_default_editor = try Sys.getenv "EDITOR" with Not_found -> "editor";
   }
 
@@ -76,6 +80,8 @@ let load_ide section =
       get_int section ~default:default_ide.ide_task_height "task_height";
     ide_verbose =
       get_int section ~default:default_ide.ide_verbose "verbose";
+    ide_saving_policy =
+      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
     ide_default_editor =
       get_string section ~default:default_ide.ide_default_editor
         "default_editor";
@@ -101,6 +107,7 @@ let load_config config =
     time_limit    = Whyconf.timelimit main;
     mem_limit     = Whyconf.memlimit main;
     verbose       = ide.ide_verbose;
+    saving_policy = ide.ide_saving_policy ;
     max_running_processes = Whyconf.running_provers_max main;
 (*
     provers = Mstr.empty;
@@ -140,6 +147,7 @@ let save_config t =
   let ide = set_int ide "tree_width" t.tree_width in
   let ide = set_int ide "task_height" t.task_height in
   let ide = set_int ide "verbose" t.verbose in
+  let ide = set_int ide "saving_policy" t.saving_policy in
   let ide = set_string ide "default_editor" t.default_editor in
   let config = set_section config "ide" ide in
 (* TODO: store newly detected provers !
@@ -149,7 +157,7 @@ let save_config t =
   save_config config
 
 let config =
-  eprintf "reading IDE config file...@?";
+  eprintf "[Info] reading IDE config file...@?";
   let c = read_config () in
   eprintf " done.@.";
   c
@@ -259,7 +267,7 @@ let resize_images size =
   ()
 
 let () =
-  eprintf "reading icons...@?";
+  eprintf "[Info] reading icons...@?";
   resize_images 20;
   eprintf " done.@."
 
@@ -341,16 +349,6 @@ let preferences c =
     GPack.vbox ~homogeneous:false ~packing:
       (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
   in
-  (* toggle show labels in formulas *)
-  let showlabels =
-    GButton.check_button ~label:"show labels in formulas" ~packing:page1#add ()
-      ~active:(set_labels_flag c.show_labels;c.show_labels)
-  in
-  let (_ : GtkSignal.id) =
-    showlabels#connect#toggled ~callback:
-      (fun () -> c.show_labels <- not c.show_labels;
-         set_labels_flag c.show_labels)
-  in
   (* editor *)
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
  let _ = GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) () in
@@ -398,6 +396,52 @@ let preferences c =
     ~packing:(fun w -> ignore(notebook#append_page
                                 ~tab_label:label2#coerce w)) ()
   in
+  (** page 3 **)
+  let set_saving_policy n () = c.saving_policy <- n in
+  let label3 = GMisc.label ~text:"IDE" () in
+  let page3 =
+    GPack.vbox ~homogeneous:false ~packing:
+      (fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) ()
+  in
+  (* session saving policy *)
+  let choice0 = 
+    GButton.radio_button 
+      ~label:"Always save on exit"
+      ~active:(c.saving_policy = 0)
+      ~packing:page3#add () 
+  in 
+  let choice1 = 
+    GButton.radio_button 
+      ~label:"Never save on exit" ~group:choice0#group
+      ~active:(c.saving_policy = 1)
+      ~packing:page3#add () 
+  in 
+  let choice2 = 
+    GButton.radio_button 
+      ~label:"ask whether to save on exit" ~group:choice0#group
+      ~active:(c.saving_policy = 2)
+      ~packing:page3#add () 
+  in 
+  let (_ : GtkSignal.id) =
+    choice0#connect#toggled ~callback:(set_saving_policy 0)
+  in
+  let (_ : GtkSignal.id) =
+    choice1#connect#toggled ~callback:(set_saving_policy 1)
+  in
+  let (_ : GtkSignal.id) =
+    choice2#connect#toggled ~callback:(set_saving_policy 2)
+  in
+  (* toggle show labels in formulas *)
+  let showlabels =
+    GButton.check_button ~label:"show labels in formulas" ~packing:page3#add ()
+      ~active:(set_labels_flag c.show_labels;c.show_labels)
+  in
+  let (_ : GtkSignal.id) =
+    showlabels#connect#toggled ~callback:
+      (fun () -> c.show_labels <- not c.show_labels;
+         set_labels_flag c.show_labels)
+  in
+  (* buttons *)
   dialog#add_button "Close" `CLOSE ;
   let ( _ : GWindow.Buttons.about) = dialog#run () in
   eprintf "saving IDE config file@.";
@@ -413,7 +457,7 @@ let run_auto_detection gconfig =
 *)
   ()
 
-let () = eprintf "end of configuration initialization@."
+let () = eprintf "[Info] end of configuration initialization@."
 
 (*
 Local Variables:

src/ide/gconfig.mli

@@ -37,6 +37,7 @@ type t =
 *)
       mutable default_editor : string;
       mutable show_labels : bool;
+      mutable saving_policy : int;
       mutable env : Why.Env.env;
       mutable config : Whyconf.config;
     }

src/ide/newmain.ml

@@ -21,7 +21,7 @@
 open Format
 
 let () =
-  eprintf "Init the GTK interface...@?";
+  eprintf "[Info] Init the GTK interface...@?";
   ignore (GtkMain.Main.init ());
   eprintf " done.@."
 
@@ -288,7 +288,7 @@ let () =
   view_time_column#set_visible true
 
 let goals_model,goals_view =
-  eprintf "Creating tree model...@?";
+  eprintf "[Info] Creating tree model...@?";
   let model = GTree.tree_store cols in
   let view = GTree.view ~model ~packing:scrollview#add () in
   let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
@@ -503,17 +503,17 @@ let project_dir, file_to_read =
     begin
       if Sys.is_directory fname then
         begin
-          eprintf "Info: found directory '%s' for the project@." fname;
+          eprintf "[Info] found directory '%s' for the project@." fname;
           fname, None
         end
       else
         begin
-          eprintf "Info: found regular file '%s'@." fname;
+          eprintf "[Info] found regular file '%s'@." fname;
           let d =
             try Filename.chop_extension fname
             with Invalid_argument _ -> fname
           in
-          eprintf "Info: using '%s' as directory for the project@." d;
+          eprintf "[Info] using '%s' as directory for the project@." d;
           d, Some (Filename.concat Filename.parent_dir_name
                      (Filename.basename fname))
         end
@@ -524,7 +524,7 @@ let project_dir, file_to_read =
 let () =
   if not (Sys.file_exists project_dir) then
     begin
-      eprintf "Info: '%s' does not exists. Creating directory of that name \
+      eprintf "[Info] '%s' does not exists. Creating directory of that name \
  for the project@." project_dir;
       Unix.mkdir project_dir 0o777
     end
@@ -532,13 +532,13 @@ let () =
 
 let () =
   try
-    eprintf "Opening session...@?";
+    eprintf "[Info] Opening session...@\n@[<v 2>  ";
     M.open_session ~env:gconfig.env 
       (* ~provers:gconfig.provers *)
       ~config:gconfig.Gconfig.config
       ~init ~notify project_dir;
     M.maximum_running_proofs := gconfig.max_running_processes;
-    eprintf " done@."
+    eprintf "@]@\n[Info] Opening session: done@."
   with e ->
     eprintf "@[Error while opening session:@ %a@.@]" 
       Exn_printer.exn_printer e;
@@ -576,7 +576,7 @@ let () =
     | None -> ()
     | Some fn ->
         if M.file_exists fn then
-          eprintf "Info: file %s already in database@." fn
+          eprintf "[Info] file %s already in database@." fn
         else
           try
             M.add_file fn
@@ -726,8 +726,12 @@ let (_ : GMenu.image_menu_item) =
     (fun () -> Gconfig.run_auto_detection gconfig; !refresh_provers () )
     ()
 
+let save_session () =
+  eprintf "[Info] saving session@.";
+  M.save_session ()
+
 let exit_function () =
-  eprintf "saving IDE config file@.";
+  eprintf "[Info] saving IDE config file@.";
   save_config ();
   (*
   eprintf "saving session (testing only)@.";
@@ -748,22 +752,29 @@ let exit_function () =
   let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
   if ret = 0 then eprintf "DTD validation succeeded, good!@.";
   *)
-  let d = GWindow.message_dialog
-    ~message:"Do you want to save the session?"
-    ~message_type:`QUESTION
-    ~buttons:GWindow.Buttons.yes_no
-    ~title:"Why3 save"
-    ~modal:true
-    ~show:true ()
-  in
-  let (_ : GtkSignal.id) =
-    d#connect#response
-      ~callback:(function x -> d#destroy ();
-                   if x = `YES then M.save_session ();
-                   GMain.quit ()
-                )
-  in
-  ()
+  match config.saving_policy with
+    | 0 -> save_session (); GMain.quit ()
+    | 1 -> GMain.quit ()
+    | 2 ->
+        let d = GWindow.message_dialog
+          ~message:"Do you want to save the session?"
+          ~message_type:`QUESTION
+          ~buttons:GWindow.Buttons.yes_no
+          ~title:"Why3 save"
+          ~modal:true
+          ~show:true ()
+        in
+        let (_ : GtkSignal.id) =
+          d#connect#response
+            ~callback:(function x -> d#destroy ();
+                         if x = `YES then save_session ();
+                         GMain.quit ()
+                      )
+        in
+        ()
+    | _ -> 
+        eprintf "unexpected value for saving_policy@.";
+        GMain.quit ()
 
 (*************)
 (* View menu *)
@@ -1186,7 +1197,7 @@ let (_ : GMenu.image_menu_item) =
 
 let (_ : GMenu.image_menu_item) =
   file_factory#add_image_item (* no shortcut ~key:GdkKeysyms._S *)
-    ~label:"_Save session" ~callback:M.save_session
+    ~label:"_Save session" ~callback:save_session
     ()
 
 
@@ -1198,7 +1209,7 @@ let save_file () =
   let f = !current_file in
   if f <> "" then
     begin
-      M.save_session ();
+      save_session ();
       let s = source_view#source_buffer#get_text () in
       let c = open_out f in
       output_string c s;

src/ide/session.ml

@@ -838,7 +838,7 @@ let rec reload_any_goal parent gid gname sum t old_goal goal_obsolete =
 and reload_trans  _goal_obsolete goal _ tr =
   let trname = tr.transf.transformation_name in
   let gname = goal.goal_name in
-  eprintf "[Reload] transformation %s for goal %s @." trname gname;
+  eprintf "[Reload] transformation %s for goal %s @\n" trname gname;
   let mtr = raw_add_transformation goal tr.transf tr.transf_expanded in
   let old_subgoals =
     List.fold_left
@@ -1021,7 +1021,7 @@ let reload_root_goal mth tname old_goals t : goal =
 
 (* reloads a theory *)
 let reload_theory mfile old_theories (_,tname,th) =
-  eprintf "[Reload] theory '%s'@."tname;
+  eprintf "[Reload] theory '%s'@\n"tname;
   let tasks = List.rev (Task.split_theory th None None) in
   let old_goals, old_exp =
     try
@@ -1068,7 +1068,7 @@ let reload_all () =
   let files = !all_files in
   let all_theories =
     List.map (fun mf ->
-                eprintf "[Reload] file '%s'@." mf.file_name;
+                eprintf "[Reload] file '%s'@\n" mf.file_name;
                 (mf,read_file mf.file_name))
       files
   in

src/ide/xml.mll

@@ -73,7 +73,7 @@ rule xml_prolog = parse
 | "<?xml" space+ "version=\"1.0\"" space+ "encoding=\"UTF-8\"" space+ "?>"
     { xml_doctype "1.0" "" lexbuf }
 | "<?xml" ([^'?']|'?'[^'>'])* "?>" 
-    { Format.eprintf "[Xml warning] prolog ignored@.";
+    { Format.eprintf "[Xml warning] prolog ignored@\n";
       xml_doctype "1.0" "" lexbuf }
 | _ 
     { parse_error "wrong prolog" }
@@ -104,13 +104,13 @@ and elements group_stack element_stack = parse
       { match group_stack with
          | [] -> 
              Format.eprintf 
-               "[Xml warning] unexpected closing Xml element `%s'@." 
+               "[Xml warning] unexpected closing Xml element `%s'@\n" 
                celem;
              elements group_stack element_stack lexbuf
          | (elem,att,stack)::g ->
              if celem <> elem then
                Format.eprintf 
-                 "[Xml warning] Xml element `%s' closed by `%s'@." 
+                 "[Xml warning] Xml element `%s' closed by `%s'@\n" 
                  elem celem;
              let e = {
                 name = elem;
@@ -120,13 +120,13 @@ and elements group_stack element_stack = parse
              in elements g (e::stack) lexbuf            
        }
   | '<'
-      { Format.eprintf "[Xml warning] unexpected '<'@.";
+      { Format.eprintf "[Xml warning] unexpected '<'@\n";
         elements group_stack element_stack lexbuf }      
   | eof 
       { match group_stack with
          | [] -> element_stack
          | (elem,_,_)::_ ->
-             Format.eprintf "[Xml warning] unclosed Xml element `%s'@." elem;
+             Format.eprintf "[Xml warning] unclosed Xml element `%s'@\n" elem;
              pop_all group_stack element_stack
       }
   | _ as c