aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-24 14:56:13 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-24 14:56:13 +0000
commit10525c0c6fce6f0d35022c6d794c787e395db667 (patch)
treee64be551812bc17876bf80faa0218926f9a9440b /ide/coqide.ml
parent8aea38ca9b526d1d1ed731948528b4e921b303d2 (diff)
tentative de completion ESC-/ a la emacs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 13d916480..058f2ca72 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 =