Adding an option to change the autocompletion delay.

3 files changed, 21 insertions, 0 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4ee5669877..d3cf08e90e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -388,6 +388,9 @@ let window_height =
 let auto_complete =
   new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool)
 
+let auto_complete_delay =
+  new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int)
+
 let stop_before =
   new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool)
 
@@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent =
       let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
       ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
     in
+    let spin text ~min ~max (pref : int preference) =
+      let box = GPack.hbox ~packing:box#pack () in
+      let but = GEdit.spin_button
+        ~numeric:true ~update_policy:`IF_VALID ~digits:0
+        ~packing:box#pack ()
+      in
+      let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in
+      let () = but#adjustment#set_bounds
+        ~lower:(float_of_int min) ~upper:(float_of_int max)
+        ~step_incr:1.
+        ()
+      in
+      let () = but#set_value (float_of_int pref#get) in
+      ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int))
+    in
     let () = button "Dynamic word wrap" dynamic_word_wrap in
     let () = button "Show line number" show_line_number in
     let () = button "Auto indentation" auto_indent in
     let () = button "Auto completion" auto_complete in
+    let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in
     let () = button "Show spaces" show_spaces in
     let () = button "Show right margin" show_right_margin in
     let () = button "Show progress bar" show_progress_bar in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 4b04326cec..7b43079b4f 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -82,6 +82,7 @@ val show_toolbar : bool preference
 val window_width : int preference
 val window_height : int preference
 val auto_complete : bool preference
+val auto_complete_delay : int preference
 val stop_before : bool preference
 val reset_on_tab_switch : bool preference
 val line_ending : line_ending preference
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 098b09601f..b7a35d7e94 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -526,6 +526,7 @@ object (self)
     stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs;
     stick tab_length self self#set_tab_width;
     stick auto_complete self self#set_auto_complete;
+    stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d);
 
     let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font self cb;