Coqide: opening non-existing files won't create them immediately anymore

 ... and many more code cleanup concerning file loading

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16034 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 88 insertions, 72 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 044cdc4abf..2f244bebb9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -27,8 +27,8 @@ class type _analyzed_view =
 object
 
   method filename : string option
-  method stats :  Unix.stats option
   method update_stats : unit
+  method changed_on_disk : bool
   method revert : unit
   method auto_save : unit
   method save : string -> bool
@@ -249,18 +249,6 @@ let get_current_word () =
       Minilib.log t;
       t
 
-let input_channel b ic =
-  let buf = String.create 1024 and len = ref 0 in
-  while len := input ic buf 0 1024; !len > 0 do
-    Buffer.add_substring b buf 0 !len
-  done
-
-let with_file handler name ~f =
-  try
-    let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
-    try f ic; close_in ic with e -> close_in ic; raise e
-  with Sys_error s -> handler s
-
 (** Cut a part of the buffer in sentences and tag them.
     May raise [Coq_lex.Unterminated] when the zone ends with
     an unterminated sentence. *)
@@ -400,18 +388,27 @@ object(self)
   val mycoqtop = _ct
 
   val mutable filename = _fn
-  val mutable stats = None
+  val mutable last_stats = NoSuchFile
   val mutable last_modification_time = 0.
   val mutable last_auto_save_time = 0.
 
   val hidden_proofs = Hashtbl.create 32
 
   method filename = filename
-  method stats = stats
-  method update_stats =
-    match filename with
-      | Some f -> stats <- my_stat f
-      | _ -> ()
+
+  method update_stats = match filename with
+    |Some f -> last_stats <- Ideutils.stat f
+    |_ -> ()
+
+  method changed_on_disk = match filename with
+    |None -> false
+    |Some f -> match Ideutils.stat f, last_stats with
+        |MTime cur_mt, MTime last_mt -> cur_mt > last_mt
+        |MTime _, (NoSuchFile|OtherError) -> true
+        |NoSuchFile, MTime _ ->
+          flash_info ("Warning, file not on disk anymore : "^f);
+          false
+        |_ -> false
 
   method revert =
     let do_revert f =
@@ -419,7 +416,7 @@ object(self)
       try
         Coq.reset_coqtop mycoqtop self#requested_reset_initial;
         let b = Buffer.create 1024 in
-        with_file flash_info f ~f:(input_channel b);
+        Ideutils.read_file f b;
         let s = try_convert (Buffer.contents b) in
         input_buffer#set_text s;
         self#update_stats;
@@ -458,8 +455,8 @@ object(self)
   method save f =
     if try_export f (input_buffer#get_text ()) then begin
       filename <- Some f;
+      self#update_stats;
       input_buffer#set_modified false;
-      stats <- my_stat f;
       (match self#auto_save_name with
         | None -> ()
         | Some fn -> try Sys.remove fn with _ -> ());
@@ -1106,7 +1103,7 @@ let current_view () = session_notebook#current_term.analyzed_view
 
 module FileAux = struct
 
-let load_file handler f =
+let load_file ?(maycreate=false) f =
   let f = CUnix.correct_path f (Sys.getcwd ()) in
   try
     Minilib.log "Loading file starts";
@@ -1121,33 +1118,27 @@ let load_file handler f =
     if not (search_f 0 session_notebook#pages) then begin
       Minilib.log "Loading: get raw content";
       let b = Buffer.create 1024 in
-      with_file handler f ~f:(input_channel b);
+      if Sys.file_exists f then Ideutils.read_file f b
+      else if not maycreate then flash_info ("Load failed: no such file");
       Minilib.log "Loading: convert content";
       let s = do_convert (Buffer.contents b) in
       Minilib.log "Loading: create view";
       let session = create_session (Some f) in
-      Minilib.log "Loading: adding view";
       let index = session_notebook#append_term session in
-      let av = session.analyzed_view in
+      session_notebook#goto_page index;
       Minilib.log "Loading: stats";
-      av#update_stats;
+      session.analyzed_view#update_stats;
       let input_buffer = session.script#buffer in
       Minilib.log "Loading: fill buffer";
       input_buffer#set_text s;
+      input_buffer#set_modified false;
       input_buffer#place_cursor ~where:input_buffer#start_iter;
       force_retag input_buffer;
-      Minilib.log ("Loading: switch to view "^ string_of_int index);
-      session_notebook#goto_page index;
-      Minilib.log "Loading: highlight";
-      input_buffer#set_modified false;
-      Minilib.log "Loading: clear undo";
       session.script#clear_undo ();
-      Minilib.log "Loading: success";
       !refresh_editor_hook ();
+      Minilib.log "Loading: success";
     end
-  with e -> handler ("Load failed: "^(Printexc.to_string e))
-
-let do_load file = load_file flash_info file
+  with e -> flash_info ("Load failed: "^(Printexc.to_string e))
 
 let confirm_save ok =
   if ok then flash_info "Saved" else warning "Save Failed"
@@ -1173,16 +1164,6 @@ let check_save ~saveas current =
       ok
   with _ -> warning "Save Failed"; false
 
-let revert {analyzed_view = av} =
-  try match av#filename,av#stats with
-    | Some f,Some stats ->
-      let new_stats = Unix.stat f in
-      if new_stats.Unix.st_mtime > stats.Unix.st_mtime
-      then av#revert
-    | Some _, None -> av#revert
-    | _ -> ()
-  with _ -> av#revert
-
 exception DontQuit
 
 let check_quit saveall =
@@ -1249,7 +1230,7 @@ let newfile _ =
 let load _ =
   match select_file_for_open ~title:"Load file" () with
     | None -> ()
-    | Some f -> FileAux.do_load f
+    | Some f -> FileAux.load_file f
 
 let save _ =
   ignore (FileAux.check_save ~saveas:false session_notebook#current_term)
@@ -1268,7 +1249,11 @@ let saveall _ =
       | Some f -> ignore (av#save f))
     session_notebook#pages
 
-let revert_all _ = List.iter FileAux.revert session_notebook#pages
+let revert_all _ =
+  List.iter
+    (function {analyzed_view = av} ->
+      if av#changed_on_disk then av#revert)
+    session_notebook#pages
 
 let quit _ =
   try FileAux.check_quit saveall; exit 0 with FileAux.DontQuit -> ()
@@ -1378,7 +1363,7 @@ let forbid_quit_to_save () =
   try FileAux.check_quit File.saveall; false
   with FileAux.DontQuit -> true
 
-let do_load = FileAux.do_load
+let do_load f = FileAux.load_file f
 
 (** Callbacks for external commands *)
 
@@ -1422,7 +1407,7 @@ let make _ =
 let next_error _ =
   try
     let file,line,start,stop,error_msg = search_next_error () in
-    FileAux.do_load file;
+    FileAux.load_file file;
     let v = session_notebook#current_term in
     let av = v.analyzed_view in
     let input_buffer = v.script#buffer in
@@ -2106,6 +2091,7 @@ let build_ui () =
   let resize_window () =
     w#resize ~width:current.window_width ~height:current.window_height
   in
+  refresh_toolbar ();
   refresh_toolbar_hook := refresh_toolbar;
   refresh_style_hook := refresh_style;
   refresh_editor_hook := refresh_editor_prefs;
@@ -2119,29 +2105,27 @@ let build_ui () =
   (* Showtime ! *)
   w#show ()
 
+let make_file_buffer f =
+  let f =
+    if Sys.file_exists f || Filename.check_suffix f ".v" then f
+    else f^".v"
+  in
+  FileAux.load_file ~maycreate:true f
+
+let make_scratch_buffer () =
+  let session = create_session None in
+  let _ = session_notebook#append_term session in
+  !refresh_editor_hook ()
+
 let main files =
   build_ui ();
   reset_revert_timer ();
   reset_autosave_timer ();
-  let do_file f =
-    if Sys.file_exists f then FileAux.do_load f
-    else
-      let f = if Filename.check_suffix f ".v" then f else f^".v" in
-      FileAux.load_file (fun s -> warning s; exit 1) f
-  in
-  begin match files with
-    |[] ->
-      let session = create_session None in
-      let index = session_notebook#append_term session in
-      !refresh_editor_hook ();
-      session_notebook#goto_page index;
-    |_ ->
-      List.iter do_file files;
-      session_notebook#goto_page 0;
-  end;
+  (match files with
+    | [] -> make_scratch_buffer ()
+    | _ -> List.iter make_file_buffer files);
+  session_notebook#goto_page 0;
   MiscMenu.initial_about ();
-  !refresh_toolbar_hook ();
-  !refresh_editor_hook ();
   session_notebook#current_term.script#misc#grab_focus ();
   Minilib.log "End of Coqide.main"
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 56a1392324..c376df99bc 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -105,9 +105,6 @@ let try_export file_name s =
     true
   with e -> Minilib.log (Printexc.to_string e);false
 
-let my_stat f = try Some (Unix.stat f) with _ -> None
-
-
 type timer = { run : ms:int -> callback:(unit->bool) -> unit;
                kill : unit -> unit }
 
@@ -340,3 +337,28 @@ let default_logger level message =
   in
   Minilib.log ~level message
 
+
+(** {6 File operations} *)
+
+(** A customized [stat] function. Exceptions are catched. *)
+
+type stats = MTime of float | NoSuchFile | OtherError
+
+let stat f =
+  try MTime (Unix.stat f).Unix.st_mtime
+  with
+    | Unix.Unix_error (Unix.ENOENT,_,_) -> NoSuchFile
+    | _ -> OtherError
+
+(** Read the content of file [f] and add it to buffer [b].
+    I/O Exceptions are propagated. *)
+
+let read_file name buf =
+  let ic = open_in name in
+  let s = String.create 1024 and len = ref 0 in
+  try
+    while len := input ic s 0 1024; !len > 0 do
+      Buffer.add_substring buf s 0 !len
+    done;
+    close_in ic
+  with e -> close_in ic; raise e
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 740a830e1c..291c0c1377 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -27,8 +27,6 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a
 
-val my_stat : string -> Unix.stats option
-
 val print_id : 'a -> unit
 
 val select_file_for_open : title:string -> unit -> string option
@@ -68,3 +66,15 @@ val textview_width : #GText.view -> int
 
 val default_logger : Interface.message_level -> string -> unit
 (** Default logger. It logs messages that the casual user should not see. *)
+
+(** {6 File operations} *)
+
+(** A customized [stat] function. Exceptions are catched. *)
+
+type stats = MTime of float | NoSuchFile | OtherError
+val stat : string -> stats
+
+(** Read the content of file [f] and add it to buffer [b].
+    I/O Exceptions are propagated. *)
+
+val read_file : string -> Buffer.t -> unit