ITP server: adding request and notif for file contents

src/ide/why3_js.ml

@@ -465,11 +465,10 @@ let onclick_do_something id =
 	else begin
 	  if not ctrl then clear_task_selection ();
           let pretty =
-            if Hashtbl.mem printed_task_list id then
-              Hashtbl.find printed_task_list id
-            else
+            try Hashtbl.find printed_task_list id
+            with Not_found ->
               (sendRequest (Get_task id);
-               "loading task")
+               "loading task, please wait")
           in (* TODO dummy value *)
           select_task id span pretty
         end;
@@ -479,10 +478,8 @@ let onclick_do_something id =
     (fun e ->
       clear_task_selection ();
       let pretty =
-          if Hashtbl.mem printed_task_list id then
-            Hashtbl.find printed_task_list id
-          else
-            (sendRequest (Get_task id); "")
+        try Hashtbl.find printed_task_list id
+        with Not_found -> (sendRequest (Get_task id); "")
       in
       select_task id span pretty;
       let x = max 0 ((e ##.clientX) - 2) in
@@ -537,6 +534,8 @@ let interpNotif (n: notification) =
       TaskList.attach_new_node nid parent ntype name detached;
       TaskList.onclick_do_something (string_of_int nid);
       sendRequest (Get_task (string_of_int nid))
+  | File_contents (_f,_s) ->
+     assert false (* TODO *)
   | Task (nid, task) ->
       Hashtbl.add TaskList.printed_task_list (string_of_int nid) task
   | Remove nid ->

src/ide/why3ide.ml

@@ -988,6 +988,7 @@ let treat_notification n = match n with
     task_view#source_buffer#set_text s;
     (* scroll to end of text *)
     task_view#scroll_to_mark `INSERT
+  | File_contents _ -> assert false (* This IDE never requests file contents *)
 
 (***********************)
 (* start the interface *)

src/session/itp_communication.ml

@@ -68,6 +68,8 @@ type notification =
   (* server exited *)
   | Task         of node_ID * string
   (* the node_ID's task *)
+  | File_contents of string * string
+  (* contents of the file *)
 
 type ide_request =
   | Command_req       of node_ID * string
@@ -77,6 +79,7 @@ type ide_request =
   | Open_session_req  of string
   | Add_file_req      of string
   | Set_max_tasks_req of int
+  | Get_file_contents of string
   | Get_task          of node_ID
   | Remove_subtree    of node_ID
   | Copy_paste        of node_ID * node_ID

src/session/itp_communication.mli

@@ -72,6 +72,8 @@ type notification =
   (* server exited *)
   | Task         of node_ID * string
   (* the node_ID's task *)
+  | File_contents of string * string
+  (* contents of the file *)
 
 type ide_request =
   | Command_req       of node_ID * string
@@ -81,6 +83,7 @@ type ide_request =
   | Open_session_req  of string
   | Add_file_req      of string
   | Set_max_tasks_req of int
+  | Get_file_contents of string
   | Get_task          of node_ID
   | Remove_subtree    of node_ID
   | Copy_paste        of node_ID * node_ID

src/session/itp_server.ml

@@ -269,6 +269,7 @@ let print_request fmt r =
   | Open_session_req f              -> fprintf fmt "open session file %s" f
   | Add_file_req f                  -> fprintf fmt "open file %s" f
   | Set_max_tasks_req i             -> fprintf fmt "set max tasks %i" i
+  | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_task _nid                   -> fprintf fmt "get task"
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
   | Copy_paste _                    -> fprintf fmt "copy paste"
@@ -303,6 +304,7 @@ let print_notify fmt n =
   | Message msg                        ->
       print_msg fmt msg
   | Dead s                             -> fprintf fmt "dead :%s" s
+  | File_contents (_f, _s)             -> fprintf fmt "file contents"
   | Task (_ni, _s)                     -> fprintf fmt "task"
 
 module type Protocol = sig
@@ -867,6 +869,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
           ignore (new_node ~parent p)
         in
         C.copy_detached ~copy d.cont from_any
+    | Get_file_contents f          ->
+       begin try let s = Sysutil.file_contents f in
+                 P.notify (File_contents(f,s))
+             with Invalid_argument s ->
+               P.notify (Message (Error s))
+       end
     | Get_task nid                 -> send_task nid
     | Replay_req                   -> replay_session (); resend_the_tree ()
     | Command_req (nid, cmd)       ->