diff options
| -rw-r--r-- | ide/coqide.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 13d916480c..058f2ca726 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2043,6 +2043,13 @@ let main files = with _ -> prerr_endline "EMIT PASTE FAILED"))); ignore (edit_f#add_separator ()); + ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback: + (do_if_not_computing + (fun () -> + ignore ( + let av = out_some ((get_current_view()).analyzed_view) in + av#complete_at_offset (av#get_insert)#offset + )))); (* let toggle_auto_complete_i = |