1 files changed, 163 insertions, 0 deletions
diff --git a/ide/coqide/wg_Completion.ml b/ide/coqide/wg_Completion.ml
new file mode 100644
index 0000000000..cc24e71386
--- /dev/null
+++ b/ide/coqide/wg_Completion.ml
@@ -0,0 +1,163 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module StringOrd =
+struct
+  type t = string
+  let compare s1 s2 =
+    (* we use first size, then usual comparison *)
+    let d = String.length s1 - String.length s2 in
+    if d <> 0 then d
+    else compare s1 s2
+end
+
+module Proposals = Set.Make(StringOrd)
+
+(** Retrieve completion proposals in the buffer *)
+let get_syntactic_completion (buffer : GText.buffer) pattern accu =
+  let rec get_aux accu (iter : GText.iter) =
+    match iter#forward_search pattern with
+    | None -> accu
+    | Some (start, stop) ->
+      if Gtk_parsing.starts_word start then
+        let ne = Gtk_parsing.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
+          let accu = Proposals.add proposal accu in
+          get_aux accu stop
+      else get_aux accu stop
+  in
+  get_aux accu buffer#start_iter
+
+(** Retrieve completion proposals in Coq libraries *)
+let get_semantic_completion pattern accu =
+  let flags = [Interface.Name_Pattern ("^" ^ pattern), true] in
+  (* Only get the last part of the qualified name *)
+  let rec last accu = function
+  | [] -> accu
+  | [basename] -> Proposals.add basename accu
+  | _ :: l -> last accu l
+  in
+  let next = function
+  | Interface.Good l ->
+    let fold accu elt = last accu elt.Interface.coq_object_qualid in
+    let ans = List.fold_left fold accu l in
+    Coq.return ans
+  | _ -> Coq.return accu
+  in
+  Coq.bind (Coq.search flags) next
+
+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
+
+class completion_provider buffer coqtop =
+  let self_provider = ref None in
+  let active = ref true in
+  let provider = object (self)
+
+    val mutable auto_complete_length = 3
+    val mutable cache = (-1, "", Proposals.empty)
+    val mutable insert_offset = -1
+
+    method name = ""
+
+    method icon = None
+
+    method private update_proposals pref =
+      let (_, _, props) = cache in
+      let filter prop = 0 <= is_substring pref prop in
+      let props = Proposals.filter filter props in
+      props
+
+    method private add_proposals ctx props =
+      let mk text =
+        let item = GSourceView3.source_completion_item ~text ~label:text () in
+        (item :> GSourceView3.source_completion_proposal)
+      in
+      let props = List.map mk (Proposals.elements props) in
+      ctx#add_proposals (Option.get !self_provider) props true
+
+    method populate ctx =
+      let iter = buffer#get_iter_at_mark `INSERT in
+      let () = insert_offset <- iter#offset in
+      let () = Minilib.log (Printf.sprintf "Completion at offset: %i" insert_offset) in
+      let buffer = new GText.buffer iter#buffer in
+      if not (Gtk_parsing.ends_word iter#backward_char) then self#add_proposals ctx Proposals.empty else
+      let start = Gtk_parsing.find_word_start iter in
+      if iter#offset - start#offset < auto_complete_length then self#add_proposals ctx Proposals.empty else
+      let w = start#get_text ~stop:iter in
+      let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in
+      let (off, prefix, props) = cache in
+      let start_offset = start#offset in
+      (* check whether we have the last request in cache *)
+      if (start_offset = off) && (0 <= is_substring prefix w) then
+        let props = self#update_proposals w in
+        self#add_proposals ctx props
+      else
+        let cancel = ref false in
+        let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in
+        let update props =
+          let () = cache <- (start_offset, w, props) in
+          if not !cancel then self#add_proposals ctx props
+        in
+        (* If not in the cache, we recompute it: first syntactic *)
+        let synt = get_syntactic_completion buffer w Proposals.empty in
+        (* Then semantic *)
+        let next props =
+          update props;
+          Coq.return ()
+        in
+        let query = Coq.bind (get_semantic_completion w synt) next in
+        (* If coqtop is computing, do the syntactic completion altogether *)
+        let occupied () = update synt in
+        Coq.try_grab coqtop query occupied
+
+    method matched ctx = !active
+
+    method activation = [`INTERACTIVE; `USER_REQUESTED]
+
+    method info_widget proposal = None
+
+    method update_info proposal info = ()
+
+    method start_iter ctx proposal iter = false
+
+    method activate_proposal proposal iter = false
+
+    method interactive_delay = (-1)
+
+    method priority = 0
+
+  end in
+  let provider = GSourceView3.source_completion_provider provider in
+  object (self)
+
+    inherit GSourceView3.source_completion_provider provider#as_source_completion_provider
+
+    method active = !active
+
+    method set_active b = active := b
+
+    initializer
+      self_provider := Some (self :> GSourceView3.source_completion_provider)
+
+  end