diff options
Diffstat (limited to 'ide/wg_ScriptView.ml')
| -rw-r--r-- | ide/wg_ScriptView.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 769ce61ee1..f2d9f33d7d 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -287,18 +287,17 @@ end class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in -let completion = new Wg_Completion.complete_model ct view#buffer in -let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in +let provider = new Wg_Completion.completion_provider ct in object (self) inherit GSourceView3.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer - method auto_complete = completion#active + method auto_complete = provider#active method set_auto_complete flag = - completion#set_active flag + provider#set_active flag method recenter_insert = self#scroll_to_mark @@ -448,7 +447,7 @@ object (self) self#buffer#delete_mark (`MARK insert_mark) - method complete_popup = popup + method proposal : string option = None (* FIXME *) method undo = undo_manager#undo method redo = undo_manager#redo @@ -527,10 +526,15 @@ 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; + let () = self#completion#set_accelerators 0 in + let () = self#completion#set_show_headers false in + let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in + () end |