Add a save file notification and edit of source in gtk.

src/ide/why3ide.ml

@@ -408,6 +408,7 @@ let reload_menu_item : GMenu.menu_item =
       clear_tree_and_table goals_model;
       send_request Reload_req)
 
+
 (* vpan222 contains:
    2.2.2.1 a notebook containing view of the current task, source code etc
    2.2.2.2 a vertiacal pan which contains
@@ -441,7 +442,8 @@ let task_view =
     ~packing:scrolled_task_view#add
     ()
 
-let source_view_table = Hstr.create 14
+let source_view_table : (int * GSourceView2.source_view) Hstr.t =
+  Hstr.create 14
 
 let create_source_view =
   let n = ref 1 in
@@ -886,6 +888,19 @@ let (_ : GMenu.menu_item) =
   exp_factory#add_item ~key:GdkKeysyms._D
     ~callback:detached_copy "Detached copy"
 
+let save_sources () =
+  Hstr.iter
+    (fun k (_n, (s: GSourceView2.source_view)) ->
+      let text_to_save = s#source_buffer#get_text () in
+      send_request (Save_file_req (k, text_to_save))
+    )
+    source_view_table
+
+(* TODO replace this with menu items *)
+let (_ : GMenu.menu_item) =
+  exp_factory#add_item ~key:GdkKeysyms._X "Save files"
+    ~callback:(fun () -> save_sources ())
+
 (*********************************)
 (* add a new file in the project *)
 (*********************************)
@@ -950,6 +965,7 @@ let treat_message_notification msg = match msg with
   | Task_Monitor (t, s, r) -> update_monitor t s r
   | Open_File_Error s      -> print_message "%s" s
   | Parse_Or_Type_Error s  -> print_message "%s" s
+  | File_Saved s           -> print_message "%s was saved" s
   | Error s                ->
       if Debug.test_flag debug then
         print_message "%s" s

src/session/itp_communication.ml

@@ -33,6 +33,7 @@ type message_notification =
   | Information           of string
   | Task_Monitor          of int * int * int
   | Parse_Or_Type_Error   of string
+  | File_Saved            of string
   | Error                 of string
   | Open_File_Error       of string
 
@@ -88,6 +89,7 @@ type ide_request =
   | Remove_subtree          of node_ID
   | Copy_paste              of node_ID * node_ID
   | Copy_detached           of node_ID
+  | Save_file_req           of string * string
   | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
   | Save_req

src/session/itp_communication.mli

@@ -38,6 +38,8 @@ type message_notification =
   (* A file was read or reloaded and now contains a parsing or typing error *)
   | Parse_Or_Type_Error   of string
   (* An error happened that could not be identified in server *)
+  | File_Saved            of string
+  (* [File_Saved f] f was saved *)
   | Error                 of string
   | Open_File_Error       of string
 
@@ -78,7 +80,7 @@ type notification =
   | Task         of node_ID * string
   (* the node_ID's task *)
   | File_contents of string * string
-  (* File_contents (name, contents) *)
+  (* File_contents (filename, contents) *)
 
 type ide_request =
   | Command_req             of node_ID * string
@@ -93,6 +95,8 @@ type ide_request =
   | Remove_subtree          of node_ID
   | Copy_paste              of node_ID * node_ID
   | Copy_detached           of node_ID
+  | Save_file_req           of string * string
+  (* Save_file_req (filename, content_of_file). Save the file *)
   | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
   | Save_req

src/session/itp_server.ml

@@ -289,6 +289,7 @@ let print_request fmt r =
   | Copy_paste _                    -> fprintf fmt "copy paste"
   | Copy_detached _                 -> fprintf fmt "copy detached"
   | Get_Session_Tree_req            -> fprintf fmt "get session tree"
+  | Save_file_req _                 -> fprintf fmt "save file"
   | Save_req                        -> fprintf fmt "save"
   | Reload_req                      -> fprintf fmt "reload"
   | Replay_req                      -> fprintf fmt "replay"
@@ -306,8 +307,9 @@ let print_msg fmt m =
   | Information s          -> fprintf fmt "info %s" s
   | Task_Monitor _         -> fprintf fmt "task montor"
   | Parse_Or_Type_Error s  -> fprintf fmt "parse_or_type_error:\n %s" s
+  | File_Saved s           -> fprintf fmt "file saved %s" s
   | Error s                -> fprintf fmt "%s" s
-  | Open_File_Error s        -> fprintf fmt "%s" s
+  | Open_File_Error s      -> fprintf fmt "%s" s
 
 let print_notify fmt n =
   match n with
@@ -413,9 +415,9 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
                        cont = c }
 
 
-  (**********************)
-  (* Read and send file *)
-  (**********************)
+  (*********************)
+  (* File input/output *)
+  (*********************)
 
   let read_and_send f =
     try
@@ -427,6 +429,18 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
     with Invalid_argument s ->
       P.notify (Message (Error s))
 
+  let save_file f file_content =
+    try
+      let d = get_server_data() in
+      let fn = Sysutil.absolutize_filename
+          (Session_itp.get_dir d.cont.controller_session) f in
+      let oc = open_out fn in
+      Printf.fprintf oc "%s\n" file_content; (* TODO replace this *)
+      close_out oc;
+      P.notify (Message (File_Saved f))
+    with Invalid_argument s ->
+      P.notify (Message (Error s))
+
 
 
   (* -----------------------------------   ------------------------------------- *)
@@ -967,6 +981,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
         C.copy_detached ~copy d.cont from_any
     | Get_file_contents f          ->
         read_and_send f
+    | Save_file_req (name, text)   ->
+        save_file name text;
     | Get_task nid                 -> send_task nid
     | Replay_req                   -> replay_session (); resend_the_tree ()
     | Command_req (nid, cmd)       ->