configure editable source views, plus backup saved files

this protects against bad behavior identified in issue #30

- user can configure whether she wants to edit files within IDE or not
- when saving a source file, a backup is created

src/ide/gconfig.ml

@@ -45,6 +45,7 @@ type t =
       mutable show_locs : bool;
       mutable show_time_limit : bool;
       mutable max_boxes : int;
+      mutable allow_source_editing : bool;
       mutable saving_policy : int;
       (** 0 = always, 1 = never, 2 = ask *)
       mutable premise_color : string;
@@ -80,6 +81,7 @@ type ide = {
   ide_show_locs : bool;
   ide_show_time_limit : bool;
   ide_max_boxes : int;
+  ide_allow_source_editing : bool;
   ide_saving_policy : int;
   ide_premise_color : string;
   ide_neg_premise_color : string;
@@ -106,6 +108,7 @@ let default_ide =
     ide_show_locs = false;
     ide_show_time_limit = false;
     ide_max_boxes = 16;
+    ide_allow_source_editing = true;
     ide_saving_policy = 2;
     ide_premise_color = "chartreuse";
     ide_neg_premise_color = "pink";
@@ -150,6 +153,8 @@ let load_ide section =
     ide_max_boxes =
       get_int section ~default:default_ide.ide_max_boxes
         "max_boxes";
+    ide_allow_source_editing =
+      get_bool section ~default:default_ide.ide_allow_source_editing "allow_source_editing";
     ide_saving_policy =
       get_int section ~default:default_ide.ide_saving_policy "saving_policy";
     ide_premise_color =
@@ -208,6 +213,7 @@ let load_config config original_config =
     show_locs     = ide.ide_show_locs ;
     show_time_limit = ide.ide_show_time_limit;
     max_boxes = ide.ide_max_boxes;
+    allow_source_editing = ide.ide_allow_source_editing ;
     saving_policy = ide.ide_saving_policy ;
     premise_color = ide.ide_premise_color;
     neg_premise_color = ide.ide_neg_premise_color;
@@ -257,6 +263,7 @@ let save_config t =
   let ide = set_bool ide "print_locs" t.show_locs in
   let ide = set_bool ide "print_time_limit" t.show_time_limit in
   let ide = set_int ide "max_boxes" t.max_boxes in
+  let ide = set_bool ide "allow_source_editing" t.allow_source_editing in
   let ide = set_int ide "saving_policy" t.saving_policy in
   let ide = set_string ide "premise_color" t.premise_color in
   let ide = set_string ide "neg_premise_color" t.neg_premise_color in
@@ -712,6 +719,15 @@ let general_settings (c : t) (notebook:GPack.notebook) =
     cntexample_check#connect#toggled ~callback:
       (fun () -> c.session_cntexample <- not c.session_cntexample)
   in
+  (* source editing allowed *)
+  let source_editing_check = GButton.check_button ~label:"allow editing source files"
+    ~packing:vb#add ()
+    ~active:c.allow_source_editing
+  in
+  let (_: GtkSignal.id) =
+    source_editing_check#connect#toggled ~callback:
+      (fun () -> c.allow_source_editing <- not c.allow_source_editing)
+  in
   (* session saving policy *)
   let set_saving_policy n () = c.saving_policy <- n in
   let saving_policy_frame =

src/ide/gconfig.mli

@@ -27,6 +27,7 @@ type t =
       mutable show_locs : bool;
       mutable show_time_limit : bool;
       mutable max_boxes : int;
+      mutable allow_source_editing : bool;
       mutable saving_policy : int;
       mutable premise_color : string;
       mutable neg_premise_color : string;

src/ide/why3ide.ml

@@ -517,6 +517,10 @@ let () =
         (Whyconf.get_provers gconfig.config);
      *)
      *)
+    Hstr.iter
+      (fun _ (_,source_view,_,_) ->
+       source_view#set_editable gconfig.allow_source_editing)
+      source_view_table;
     send_session_config_to_server ()
   in
   connect_menu_item menu_preferences ~callback
@@ -815,7 +819,7 @@ let create_source_view =
             ~show_line_numbers:true
             ~right_margin_position:80 ~show_right_margin:true
             (* ~smart_home_end:true *)
-            ~editable:true
+            ~editable:gconfig.allow_source_editing
             ~packing:scrolled_source_view#add
             () in
         let has_changed = ref false in

src/session/itp_server.ml

@@ -611,7 +611,8 @@ end
     try
       let d = get_server_data() in
       let fn = Sysutil.absolutize_filename
-          (Session_itp.get_dir d.cont.controller_session) f in
+                 (Session_itp.get_dir d.cont.controller_session) f in
+      Sysutil.backup_file fn;
       Sysutil.write_file fn file_content;
       P.notify (Message (File_Saved f))
     with Invalid_argument s ->