aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-03 08:48:30 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-03 08:48:30 +0200
commitb667f6fec675d3a05ba0475bdb84beaeed7622ac (patch)
tree46923bcb0238d744e66c4acf4dcbb67d40d5b0c3 /ide/ideutils.ml
parent6950837dd6e2a3a2bc3c3d748d06054a625bc661 (diff)
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.
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml24
1 files changed, 13 insertions, 11 deletions
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