diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-03 08:48:30 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-03 08:48:30 +0200 |
commit | b667f6fec675d3a05ba0475bdb84beaeed7622ac (patch) | |
tree | 46923bcb0238d744e66c4acf4dcbb67d40d5b0c3 /ide/ideutils.ml | |
parent | 6950837dd6e2a3a2bc3c3d748d06054a625bc661 (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.ml | 24 |
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 |