Use the directory of the current session for selecting files to open.

The old behavior was extremely annoying, especially when using coqide from
the command line, since the "open" box would then point to a seemingly
random point of the filesystem rather than to the directory of the files
currently being edited (since they were passed on the command line rather
than by point-and-click).

The new behavior matches the one of mainstream editors, e.g. emacs, gedit.

3 files changed, 19 insertions, 14 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index eb994fe8e..0f4cb7b07 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -253,11 +253,14 @@ let newfile _ =
   !refresh_editor_hook ();
   notebook#goto_page index
 
-let load _ =
-  match select_file_for_open ~title:"Load file" () with
+let load sn =
+  let filename = sn.fileops#filename in
+  match select_file_for_open ~title:"Load file" ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
+let load = cb_on_current_term load
+
 let save _ = on_current_term (FileAux.check_save ~saveas:false)
 
 let saveas sn =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 973ff0b77..67e4bdb0c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -144,8 +144,7 @@ let current_dir () = match current.project_path with
 | None -> ""
 | Some dir -> dir
 
-let select_file_for_open ~title () =
-  let file = ref None in
+let select_file_for_open ~title ?filename () =
   let file_chooser =
     GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
   in
@@ -154,19 +153,22 @@ let select_file_for_open ~title () =
   file_chooser#add_filter (filter_coq_files ());
   file_chooser#add_filter (filter_all_files ());
   file_chooser#set_default_response `OPEN;
-  ignore (file_chooser#set_current_folder (current_dir ()));
-  begin match file_chooser#run () with
+  let dir = match filename with
+    | None -> current_dir ()
+    | Some f -> Filename.dirname f in
+  ignore (file_chooser#set_current_folder dir);
+  let file =
+    match file_chooser#run () with
     | `OPEN ->
       begin
-	file := file_chooser#filename;
-	match !file with
-	  | None -> ()
-	  | Some s -> current.project_path <- file_chooser#current_folder
+	match file_chooser#filename with
+	  | None -> None
+	  | Some _ as f ->
+            current.project_path <- file_chooser#current_folder; f
       end
-    | `DELETE_EVENT | `CANCEL -> ()
-  end ;
+    | `DELETE_EVENT | `CANCEL -> None in
   file_chooser#destroy ();
-  !file
+  file
 
 let select_file_for_save ~title ?filename () =
   let file = ref None in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index c2b51dd39..1fb30e4d7 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
 val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 
-val select_file_for_open : title:string -> unit -> string option
+val select_file_for_open : title:string -> ?filename:string -> unit -> string option
 val select_file_for_save :
   title:string -> ?filename:string -> unit -> string option
 val try_convert : string -> string