Rewritten the autocompletion mechanism of CoqIDE, and stuffed it

into the ScriptView widget. The autocompletion algorithm may be a
bit too greedy, so there are tests to do on huge buffers to check
whether it is too slow and therefore we should fine-tune it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15282 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 92 insertions, 0 deletions

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 64f7da101..cbc8212e9 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -8,6 +8,8 @@
 
 open Ideutils
 open GText
+open Gtk_parsing
+
 type action =
   | Insert of string * int * int (* content*pos*length *)
   | Delete of string * int * int (* content*pos*length *)
@@ -18,15 +20,60 @@ let neg act = match act with
 
 type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
 
+let is_substring s1 s2 =
+  let s1 = Glib.Utf8.to_unistring s1 in
+  let s2 = Glib.Utf8.to_unistring s2 in
+  let break = ref true in
+  let i = ref 0 in
+  let len1 = Array.length s1 in
+  let len2 = Array.length s2 in
+  while !break && !i < len1 & !i < len2 do
+    break := s1.(!i) = s2.(!i);
+    incr i;
+  done;
+  if !break then len2 - len1
+  else -1
+
+module StringOrd =
+struct
+  type t = string
+  let compare = Pervasives.compare
+end
+
+module Proposals = Set.Make(StringOrd)
+
+let get_completion (buffer : GText.buffer) w =
+  let rec get_aux accu (iter : GText.iter) =
+    match iter#forward_search w with
+    | None -> accu
+    | Some (start, stop) ->
+      if starts_word start then
+        let ne = find_word_end stop in
+        if ne#compare stop = 0 then get_aux accu stop
+        else
+          let proposal = buffer#get_text ~start ~stop:ne () in
+          get_aux (Proposals.add proposal accu) stop
+      else get_aux accu stop
+  in
+  get_aux Proposals.empty buffer#start_iter
+
 class script_view (tv : source_view) =
 object (self)
   inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
 
   val mutable history = []
   val mutable redo = []
+  val mutable auto_complete = false
+  val mutable auto_complete_length = 3
+  val mutable last_completion = (-1, "", Proposals.empty)
 
   val undo_lock = Mutex.create ()
 
+  method auto_complete = auto_complete
+
+  method set_auto_complete flag =
+    auto_complete <- flag
+
   method private dump_debug () =
     let iter = function
     | Insert (s, p, l) ->
@@ -114,9 +161,54 @@ object (self)
       Mutex.unlock undo_lock
     end
 
+  method private do_auto_complete () =
+    let iter = self#buffer#get_iter `INSERT in
+    prerr_endline ("Completion at offset: " ^ string_of_int iter#offset);
+    let start = find_word_start iter in
+    if ends_word iter#backward_char then begin
+      let w = self#buffer#get_text ~start ~stop:iter () in
+      if String.length w >= auto_complete_length then begin
+        prerr_endline ("Completion of prefix: '" ^ w ^ "'");
+        let (off, prefix, proposals) = last_completion in
+        let new_proposals = 
+        (* check whether we have the last request in cache *)
+          if (start#offset = off) && (0 <= is_substring prefix w) then
+            Proposals.filter (fun p -> 0 < is_substring w p) proposals
+          else
+            let ans = get_completion self#buffer w in
+            let () = last_completion <- (start#offset, w, ans) in
+            ans
+        in
+        let prop =
+          try Some (Proposals.choose new_proposals)
+          with Not_found -> None
+        in
+        match prop with
+        | None -> ()
+        | Some proposal ->
+          let suffix =
+            let len1 = String.length proposal in
+            let len2 = String.length w in
+            String.sub proposal len2 (len1 - len2)
+          in
+          let offset = iter#offset in
+          ignore (self#buffer#delete_selection ());
+          ignore (self#buffer#insert_interactive suffix);
+          let ins = self#buffer#get_iter (`OFFSET offset) in
+          let sel = self#buffer#get_iter `INSERT in
+          self#buffer#select_range sel ins
+      end
+    end
+
+  method private may_auto_complete iter s =
+    if auto_complete then self#do_auto_complete ()
+
   initializer
+    (* Install undo managing *)
     ignore (self#buffer#connect#insert_text ~callback:self#handle_insert);
     ignore (self#buffer#connect#delete_range ~callback:self#handle_delete);
+    (* Install auto-completion *)
+    ignore (self#buffer#connect#after#insert_text ~callback:self#may_auto_complete);
     (* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *)
     ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
     ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));