aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/wg_Completion.ml31
-rw-r--r--ide/wg_Completion.mli4
-rw-r--r--ide/wg_ScriptView.ml2
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