From e4b1478b055a7e88db4de1910b4bd90a48a3aacb Mon Sep 17 00:00:00 2001 From: Sylvain Dailler Date: Tue, 11 Apr 2017 21:54:56 +0200 Subject: [PATCH] Add a save file notification and edit of source in gtk. --- src/ide/why3ide.ml | 18 +++++++++++++++++- src/session/itp_communication.ml | 2 ++ src/session/itp_communication.mli | 6 +++++- src/session/itp_server.ml | 24 ++++++++++++++++++++---- 4 files changed, 44 insertions(+), 6 deletions(-) diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index 94f16fb7a..c017ff1df 100644 --- a/src/ide/why3ide.ml +++ b/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 diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml index 239c41dbc..aa497cdc7 100644 --- a/src/session/itp_communication.ml +++ b/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 diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli index 8433b1460..30ee29ffe 100644 --- a/src/session/itp_communication.mli +++ b/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 diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 25ef00c6e..9145283cd 100644 --- a/src/session/itp_server.ml +++ b/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) -> -- GitLab