From b667f6fec675d3a05ba0475bdb84beaeed7622ac Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 3 Apr 2015 08:48:30 +0200
Subject: 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.
---
 ide/ideutils.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'ide/ideutils.ml')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 973ff0b778..67e4bdb0c9 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
-- 
cgit v1.2.3