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/coqide.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/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 7 |
1 files changed, 5 insertions, 2 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 = |