diff options
| -rw-r--r-- | ide/wg_Completion.ml | 31 | ||||
| -rw-r--r-- | ide/wg_Completion.mli | 4 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 2 |
3 files changed, 29 insertions, 8 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 39c695f21..c34190c8a 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -109,7 +109,7 @@ object (self) (* disable autocomplete *) is_auto_completing <- false - method store = (filtered_store :> GTree.model) + method store = filtered_store method column = column @@ -289,10 +289,34 @@ object (self) let () = model#handle_proposal path in self#hide () + method private manage_scrollbar () = + (** HACK: we don't have access to the treeview size because of the lack of + LablGTK binding for certain functions, so we bypass it by approximating + it through the size of the proposals *) + let height = match model#store#get_iter_first with + | None -> -1 + | Some iter -> + let path = model#store#get_path iter in + let area = data#get_cell_area ~path ~col () in + let height = Gdk.Rectangle.height area in + let height = 16 * height in + height + in + let len = ref 0 in + let () = model#store#foreach (fun _ _ -> incr len; false) in + if !len > 15 then + let () = frame#set_vpolicy `ALWAYS in + data#misc#set_size_request ~height () + else + data#misc#set_size_request ~height:(-1) () + method private refresh () = - let () = obj#resize 1 1 in + let () = frame#set_vpolicy `NEVER in +(* let () = obj#resize 1 1 in *) let () = self#select_first () in - obj#misc#show () + let () = obj#misc#show () in + let () = self#manage_scrollbar () in + obj#resize 1 1 method private start_callback off = let (x, y, w, h) = self#coordinates (`OFFSET off) in @@ -300,7 +324,6 @@ object (self) () method private update_callback off word props = - let () = frame#set_vpolicy `NEVER in if Proposals.is_empty props then self#hide () else if Proposals.mem word props then self#hide () else self#refresh () diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index cf6773175..e34cc826a 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module Proposals : Set.S with type elt = string +module Proposals : sig type t end class complete_model : Coq.coqtop -> GText.buffer -> object method active : bool method set_active : bool -> unit - method store : GTree.model + method store : GTree.model_filter method column : string GTree.column method handle_proposal : Gtk.tree_path -> unit method start_completion_callback : (int -> unit) -> unit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 464f8f949..6d7dc6bcc 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -85,8 +85,6 @@ let rec negate_action act = match act with type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj -module Proposals = Wg_Completion.Proposals - class undo_manager (buffer : GText.buffer) = object(self) val mutable lock_undo = true |