aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml7
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 =