diff options
| -rw-r--r-- | ide/coqide.ml | 7 | ||||
| -rw-r--r-- | ide/ideutils.ml | 24 | ||||
| -rw-r--r-- | ide/ideutils.mli | 2 |
3 files changed, 19 insertions, 14 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index eb994fe8e8..0f4cb7b073 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 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 diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c2b51dd396..1fb30e4d72 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 |