diff options
| -rw-r--r-- | ide/preferences.ml | 19 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 1 |
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; |