Monadification of coqtop queries in CoqIDE

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

6 files changed, 277 insertions, 201 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 9baf3c782..d31ed9d1b 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -280,6 +280,18 @@ type coqtop = {
   mutable status : status;
 }
 
+let return (x : 'a) : 'a task =
+  (); fun _ k -> k x
+
+let bind (m : 'a task) (f : 'a -> 'b task) : 'b task =
+  (); fun h k -> m h (fun x -> f x h k)
+
+let seq (m : unit task) (n : 'a task) : 'a task =
+  (); fun h k -> m h (fun () -> n h k)
+
+let lift (f : unit -> 'a) : 'a task =
+  (); fun _ k -> k (f ())
+
 (** * Starting / signaling / ending a real coqtop sub-process *)
 
 (** We simulate a Unix.open_process that also returns the pid of
diff --git a/ide/coq.mli b/ide/coq.mli
index 230ff0b0b..a666c3cc2 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -49,7 +49,19 @@ type handle
 *)
 
 type void
-type 'a task = handle -> ('a -> void) -> void
+type 'a task
+
+val return : 'a -> 'a task
+(** Monadic return of values as tasks. *)
+
+val bind : 'a task -> ('a -> 'b task) -> 'b task
+(** Monadic binding of tasks *)
+
+val lift : (unit -> 'a) -> 'a task
+(** Return the impertative computation waiting to be processed. *)
+
+val seq : unit task -> 'a task -> 'a task
+(** Sequential composition *)
 
 (** Check if coqtop is computing, i.e. already has a current task *)
 val is_computing : coqtop -> bool
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c41db3e2d..3e76b94b2 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -19,6 +19,9 @@ type ide_info = {
 
 let prefs = Preferences.current
 
+let log msg : unit task =
+  Coq.lift (fun () -> Minilib.log msg)
+
 class type ops =
 object
   method go_to_insert : unit task
@@ -51,34 +54,40 @@ object(self)
   method private get_insert =
     buffer#get_iter_at_mark `INSERT
 
-  method show_goals h k =
+  method show_goals =
     Coq.PrintOpt.set_printing_width proof#width;
-    Coq.goals h (function
-      |Interface.Fail (l, str) ->
-        (messages#set ("Error in coqtop:\n"^str); k())
-      |Interface.Good goals | Interface.Unsafe goals ->
-        Coq.evars h (function
-          |Interface.Fail (l, str)->
-            (messages#set ("Error in coqtop:\n"^str); k())
-          |Interface.Good evs | Interface.Unsafe evs ->
-            proof#set_goals goals;
-            proof#set_evars evs;
-            proof#refresh ();
-            k()))
+    Coq.bind Coq.goals (function
+    | Interface.Fail (l, str) ->
+      messages#set ("Error in coqtop:\n"^str);
+      Coq.return ()
+    | Interface.Good goals | Interface.Unsafe goals ->
+      Coq.bind Coq.evars (function
+        | Interface.Fail (l, str)->
+          messages#set ("Error in coqtop:\n"^str);
+          Coq.return ()
+        | Interface.Good evs | Interface.Unsafe evs ->
+          proof#set_goals goals;
+          proof#set_evars evs;
+          proof#refresh ();
+          Coq.return ()
+        )
+      )
 
   (* This method is intended to perform stateless commands *)
-  method raw_coq_query phrase h k =
-    let () = Minilib.log "raw_coq_query starting now" in
+  method raw_coq_query phrase =
+    let action = log "raw_coq_query starting now" in
     let display_error s =
       if not (Glib.Utf8.validate s) then
         flash_info "This error is so nasty that I can't even display it."
       else messages#add s;
     in
-    Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase h
-      (function
-        | Interface.Fail (_, err) -> display_error err; k ()
-        | Interface.Good msg | Interface.Unsafe msg ->
-          messages#add msg; k ())
+    let query = Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase in
+    let next = function
+    | Interface.Fail (_, err) -> display_error err; Coq.return ()
+    | Interface.Good msg | Interface.Unsafe msg ->
+      messages#add msg; Coq.return ()
+    in
+    Coq.bind (Coq.seq action query) next
 
   (** [fill_command_queue until q] fills a command queue until the [until]
       condition returns true; it is fed with the number of phrases read and the
@@ -131,7 +140,8 @@ object(self)
     ignore (Queue.pop queue);
     Stack.push sentence cmd_stack
 
-  method private process_error queue phrase loc msg h k =
+  method private process_error queue phrase loc msg =
+    Coq.bind (Coq.return ()) (function () ->
     let position_error = function
       | None -> ()
       | Some (start, stop) ->
@@ -148,27 +158,30 @@ object(self)
     position_error loc;
     messages#clear;
     messages#push Interface.Error msg;
-    self#show_goals h k
+    self#show_goals)
 
   (** Compute the phrases until [until] returns [true]. *)
-  method private process_until until verbose h k =
-    let queue = Queue.create () in
-    (* Lock everything and fill the waiting queue *)
-    push_info "Coq is computing";
-    messages#clear;
-    script#set_editable false;
-    self#fill_command_queue until queue;
-    (* Now unlock and process asynchronously. Since [until]
-       may contain iterators, it shouldn't be used anymore *)
-    script#set_editable true;
-    let push_info lvl msg = if verbose then messages#push lvl msg
+  method private process_until until verbose =
+    let push_msg lvl msg = if verbose then messages#push lvl msg in
+    let action = Coq.lift (fun () ->
+      let queue = Queue.create () in
+      (* Lock everything and fill the waiting queue *)
+      push_info "Coq is computing";
+      messages#clear;
+      script#set_editable false;
+      self#fill_command_queue until queue;
+      (* Now unlock and process asynchronously. Since [until]
+        may contain iterators, it shouldn't be used anymore *)
+      script#set_editable true;
+      Minilib.log "Begin command processing";
+      queue)
     in
-    Minilib.log "Begin command processing";
+    Coq.bind action (fun queue ->
     let rec loop () =
       if Queue.is_empty queue then
         let () = pop_info () in
         let () = script#recenter_insert in
-        self#show_goals h k
+        self#show_goals
       else
         let sentence = Queue.peek queue in
         if List.mem `COMMENT sentence.flags then
@@ -181,33 +194,37 @@ object(self)
             start#get_slice ~stop
           in
           let commit_and_continue msg flags =
-            push_info Interface.Notice msg;
+            push_msg Interface.Notice msg;
             self#commit_queue_transaction queue sentence flags;
             loop ()
           in
-          Coq.interp ~logger:push_info ~verbose phrase h
-            (function
-              |Interface.Good msg -> commit_and_continue msg []
-              |Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
-              |Interface.Fail (loc, msg) ->
-                self#process_error queue phrase loc msg h k)
+          let query = Coq.interp ~logger:push_msg ~verbose phrase in
+          let next = function
+          | Interface.Good msg -> commit_and_continue msg []
+          | Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
+          | Interface.Fail (loc, msg) ->
+            self#process_error queue phrase loc msg
+          in
+          Coq.bind query next
     in
-    loop ()
+    loop ())
 
-  method process_next_phrase h k =
+  method process_next_phrase =
     let until len start stop = 1 <= len in
-    self#process_until until true h
-      (fun () -> buffer#place_cursor ~where:self#get_start_of_input; k())
+    let next () =
+      buffer#place_cursor ~where:self#get_start_of_input; Coq.return ()
+    in
+    Coq.bind (self#process_until until true) next
 
-  method private process_until_iter iter h k =
+  method private process_until_iter iter =
     let until len start stop =
       if prefs.Preferences.stop_before then stop#compare iter > 0
       else start#compare iter >= 0
     in
-    self#process_until until false h k
+    self#process_until until false
 
-  method process_until_end_or_error h k =
-    self#process_until_iter buffer#end_iter h k
+  method process_until_end_or_error =
+    self#process_until_iter buffer#end_iter
 
   (** Clear the command stack until [until] returns [true].
       Returns the number of commands sent to Coqtop to backtrack. *)
@@ -248,53 +265,60 @@ object(self)
       buffer#delete_mark stop_mark
 
   (** Actually performs the undoing *)
-  method private undo_command_stack n clear_zone h k =
-    Coq.rewind n h (function
-      |Interface.Good n | Interface.Unsafe n ->
-        let until _ len _ _ = n <= len in
-        (* Coqtop requested [n] more ACTUAL backtrack *)
-        let _, zone = self#prepare_clear_zone until clear_zone in
-        self#commit_clear_zone zone;
-        k ()
-      |Interface.Fail (l, str) ->
-        messages#set
-          ("Error while backtracking: " ^ str ^
-           "\nCoqIDE and coqtop may be out of sync," ^
-           "you may want to use Restart.");
-        k ())
+  method private undo_command_stack n clear_zone =
+    let next = function
+    | Interface.Good n | Interface.Unsafe n ->
+      let until _ len _ _ = n <= len in
+      (* Coqtop requested [n] more ACTUAL backtrack *)
+      let _, zone = self#prepare_clear_zone until clear_zone in
+      self#commit_clear_zone zone;
+      Coq.return ()
+    | Interface.Fail (l, str) ->
+      messages#set
+        ("Error while backtracking: " ^ str ^
+          "\nCoqIDE and coqtop may be out of sync," ^
+          "you may want to use Restart.");
+      Coq.return ()
+    in
+    Coq.bind (Coq.rewind n) next
 
   (** Wrapper around the raw undo command *)
-  method private backtrack_until until h k =
-    push_info "Coq is undoing";
-    messages#clear;
+  method private backtrack_until until =
+    let action () = 
+      push_info "Coq is undoing";
+      messages#clear
+    in
+    Coq.bind (Coq.lift action) (fun () ->
     (* Instead of locking the whole buffer, we now simply remove
        read-only tags *after* the actual backtrack *)
-    let to_undo,zone = self#prepare_clear_zone until None in
-    self#undo_command_stack to_undo zone h
-      (fun () -> pop_info (); k ())
+      let to_undo, zone = self#prepare_clear_zone until None in
+      let next () = pop_info (); Coq.return () in
+      Coq.bind (self#undo_command_stack to_undo zone) next
+    )
 
-  method private backtrack_to_iter iter h k =
+  method private backtrack_to_iter iter =
     let until _ _ _ stop =
       iter#compare (buffer#get_iter_at_mark stop) >= 0
     in
-    self#backtrack_until until h
+    Coq.seq (self#backtrack_until until)
       (* We may have backtracked too much: let's replay *)
-      (fun () -> self#process_until_iter iter h k)
+      (self#process_until_iter iter)
 
-  method backtrack_last_phrase h k =
+  method backtrack_last_phrase =
     let until len _ _ _ = 1 <= len in
-    self#backtrack_until until h
+    Coq.bind (self#backtrack_until until)
       (fun () ->
         buffer#place_cursor ~where:self#get_start_of_input;
-        self#show_goals h k)
+        self#show_goals)
 
-  method go_to_insert h k =
+  method go_to_insert =
+    Coq.bind (Coq.return ()) (fun () ->
     let point = self#get_insert in
     if point#compare self#get_start_of_input >= 0
-    then self#process_until_iter point h k
-    else self#backtrack_to_iter point h k
+    then self#process_until_iter point
+    else self#backtrack_to_iter point)
 
-  method tactic_wizard l h k =
+  method tactic_wizard l =
     let insert_phrase phrase tag =
       let stop = self#get_start_of_input in
       let phrase' = if stop#starts_line then phrase else "\n"^phrase in
@@ -312,7 +336,7 @@ object(self)
       } in
       Stack.push ide_payload cmd_stack;
       messages#clear;
-      self#show_goals h k;
+      self#show_goals
     in
     let display_error (loc, s) =
       if not (Glib.Utf8.validate s) then
@@ -320,67 +344,82 @@ object(self)
       else messages#add s
     in
     let try_phrase phrase stop more =
-      Minilib.log "Sending to coq now";
-      Coq.interp ~verbose:false phrase h
-        (function
-          |Interface.Fail (l, str) ->
-            display_error (l, str);
-            messages#add ("Unsuccessfully tried: "^phrase);
-            more ()
-          |Interface.Good msg ->
-            messages#add msg;
-            stop Tags.Script.processed
-          |Interface.Unsafe msg ->
-            messages#add msg;
-            stop Tags.Script.unjustified)
+      let action = log "Sending to coq now" in
+      let query = Coq.interp ~verbose:false phrase in
+      let next = function
+      | Interface.Fail (l, str) ->
+        display_error (l, str);
+        messages#add ("Unsuccessfully tried: "^phrase);
+        more
+      | Interface.Good msg ->
+        messages#add msg;
+        stop Tags.Script.processed
+      | Interface.Unsafe msg ->
+        messages#add msg;
+        stop Tags.Script.unjustified
+      in
+      Coq.bind (Coq.seq action query) next
     in
-    let rec loop l () = match l with
-      | [] -> k ()
+    let rec loop l = match l with
+      | [] -> Coq.return ()
       | p :: l' ->
         try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
     in
-    loop l ()
-
-  method handle_reset_initial why h k =
-    if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
-    (* clear the stack *)
-    while not (Stack.is_empty cmd_stack) do
-      let phrase = Stack.pop cmd_stack in
-      buffer#delete_mark phrase.start;
-      buffer#delete_mark phrase.stop
-    done;
-    (* reset the buffer *)
-    buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
-    Sentence.tag_all buffer;
-    (* clear the views *)
-    messages#clear;
-    proof#clear ();
-    clear_info ();
-    push_info "Restarted";
-    (* apply the initial commands to coq *)
-    self#initialize h k;
-
-  method private include_file_dir_in_path h k =
-    match get_filename () with
-      |None -> k ()
-      |Some f ->
-        let dir = Filename.dirname f in
-        Coq.inloadpath dir h (function
-          |Interface.Fail (_,s) ->
-            messages#set
-              ("Could not determine lodpath, this might lead to problems:\n"^s);
-            k ()
-          |Interface.Good true |Interface.Unsafe true -> k ()
-          |Interface.Good false |Interface.Unsafe false ->
-            let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-            Coq.interp cmd h (function
-              |Interface.Fail (l,str) ->
-                messages#set ("Couln't add loadpath:\n"^str);
-                k ()
-              |Interface.Good _ | Interface.Unsafe _ -> k ()))
-
-  method initialize h k =
-    self#include_file_dir_in_path h
-      (fun () -> Coq.PrintOpt.enforce h k)
+    loop l
+
+  method handle_reset_initial why =
+    let action () =
+      if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
+      (* clear the stack *)
+      while not (Stack.is_empty cmd_stack) do
+        let phrase = Stack.pop cmd_stack in
+        buffer#delete_mark phrase.start;
+        buffer#delete_mark phrase.stop
+      done;
+      (* reset the buffer *)
+      buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
+      Sentence.tag_all buffer;
+      (* clear the views *)
+      messages#clear;
+      proof#clear ();
+      clear_info ();
+      push_info "Restarted";
+      (* apply the initial commands to coq *)
+    in
+    Coq.seq (Coq.lift action) self#initialize
+
+  method private include_file_dir_in_path =
+    let query f =
+      let dir = Filename.dirname f in
+      let loadpath = Coq.inloadpath dir in
+      let next = function
+      | Interface.Fail (_, s) ->
+        messages#set
+          ("Could not determine lodpath, this might lead to problems:\n"^s);
+        Coq.return ()
+      | Interface.Good true | Interface.Unsafe true -> Coq.return ()
+      | Interface.Good false | Interface.Unsafe false ->
+        let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
+        let cmd = Coq.interp cmd in
+        let next = function
+        | Interface.Fail (l, str) ->
+          messages#set ("Couln't add loadpath:\n"^str);
+          Coq.return ()
+        | Interface.Good _ | Interface.Unsafe _ ->
+          Coq.return ()
+        in
+        Coq.bind cmd next
+      in
+      Coq.bind loadpath next
+    in
+    let next () = match get_filename () with
+    | None -> Coq.return ()
+    | Some f -> query f
+    in
+    Coq.bind (Coq.return ()) next
+
+  method initialize =
+    let next () = Coq.PrintOpt.enforce in
+    Coq.bind self#include_file_dir_in_path next
 
 end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d48e7d4a5..bb3114569 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -474,22 +474,25 @@ end
 
 (** Callbacks for the Navigation menu *)
 
-let update_status h k =
-  let display msg = pop_info (); push_info msg
+let update_status =
+  let display msg = pop_info (); push_info msg in
+  let next = function
+  | Interface.Fail (l, str) ->
+    display "Oops, problem while fetching coq status.";
+    Coq.return ()
+  | Interface.Good status | Interface.Unsafe status ->
+    let path = match status.Interface.status_path with
+      | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+      | _ :: l -> " in " ^ String.concat "." l
+    in
+    let name = match status.Interface.status_proofname with
+      | None -> ""
+      | Some n -> ", proving " ^ n
+    in
+    display ("Ready" ^ path ^ name);
+    Coq.return ()
   in
-  Coq.status h (function
-    |Interface.Fail (l, str) ->
-      display "Oops, problem while fetching coq status."; k ()
-    |Interface.Good status | Interface.Unsafe status ->
-      let path = match status.Interface.status_path with
-        | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
-        | _ :: l -> " in " ^ String.concat "." l
-      in
-      let name = match status.Interface.status_proofname with
-        | None -> ""
-        | Some n -> ", proving " ^ n
-      in
-      display ("Ready" ^ path ^ name); k ())
+  Coq.bind Coq.status next
 
 let find_next_occurrence ~backward =
   (** go to the next occurrence of the current word, forward or backward *)
@@ -507,7 +510,7 @@ let find_next_occurrence ~backward =
 let send_to_coq f =
   let sn = notebook#current_term in
   let info () = Minilib.log ("Coq busy, discarding query") in
-  let f h k = f sn h (fun () -> update_status h k) in
+  let f = Coq.seq (f sn) update_status in
   Coq.try_grab sn.coqtop f info
 
 module Nav = struct
@@ -555,9 +558,10 @@ let print_branches c cases =
   Format.fprintf c "@[match var with@\n%aend@]@."
     (print_list print_branch) cases
 
-let display_match k = function
-  |Interface.Fail _ -> flash_info "Not an inductive type"; k ()
-  |Interface.Good cases |Interface.Unsafe cases ->
+let display_match = function
+  |Interface.Fail _ ->
+    flash_info "Not an inductive type"; Coq.return ()
+  |Interface.Good cases | Interface.Unsafe cases ->
     let text =
       let buf = Buffer.create 1024 in
       let () = print_branches (Format.formatter_of_buffer buf) cases in
@@ -574,12 +578,13 @@ let display_match k = function
       b#move_mark ~where:(i#backward_chars 3) `SEL_BOUND
     end;
     b#delete_mark (`MARK m);
-    k ()
+    Coq.return ()
 
 let match_callback _ =
   let w = get_current_word () in
   let coqtop = notebook#current_term.coqtop in
-  Coq.try_grab coqtop (fun h k -> Coq.mkcases w h (display_match k)) ignore
+  let query = Coq.bind (Coq.mkcases w) display_match in
+  Coq.try_grab coqtop query ignore
 
 (** Queries *)
 
@@ -598,13 +603,14 @@ let searchabout () =
     buf#insert tpe;
     buf#insert "\n";
   in
-  let display_results k r =
+  let display_results r =
     sn.messages#clear;
     List.iter insert (match r with Interface.Good l -> l | _ -> []);
-    k ()
+    Coq.return ()
   in
-  let launch_query h k =
-    Coq.search [Interface.SubType_Pattern word, true] h (display_results k)
+  let launch_query =
+    let search = Coq.search [Interface.SubType_Pattern word, true] in
+    Coq.bind search display_results
   in
   Coq.try_grab sn.coqtop launch_query ignore
 
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 98ce63faf..e0a742779 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -113,14 +113,14 @@ object(self)
       in
       let log level message = result#buffer#insert (message^"\n")
       in
-      let process h k =
-	Coq.interp ~logger:log ~raw:true phrase h (function
-          |Interface.Fail (l,str) ->
+      let process =
+	Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function
+          | Interface.Fail (l,str) ->
             result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
-	    k ()
-          |Interface.Good res | Interface.Unsafe res ->
+	    Coq.return ()
+          | Interface.Good res | Interface.Unsafe res ->
             result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
-	    k ())
+	    Coq.return ())
       in
       result#buffer#set_text "";
       Coq.try_grab coqtop process ignore
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index c72f52484..0b9c3750c 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -107,9 +107,10 @@ end
 
 module Proposals = Set.Make(StringOrd)
 
-let get_completion (buffer : GText.buffer) coqtop w handle_res =
+(** 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 w with
+    match iter#forward_search pattern with
     | None -> accu
     | Some (start, stop) ->
       if starts_word start then
@@ -117,29 +118,29 @@ let get_completion (buffer : GText.buffer) coqtop w handle_res =
         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
+          let accu = Proposals.add proposal accu in
+          get_aux accu stop
       else get_aux accu stop
   in
-  let get_semantic accu =
-    let flags = [Interface.Name_Pattern ("^" ^ w), true] in
-    let query h k =
-      Coq.search flags h
-	(function
-	  | Interface.Good l ->
-	    let fold accu elt =
-              let rec last accu = function
-		| [] -> accu
-		| [basename] -> Proposals.add basename accu
-		| _ :: l -> last accu l
-              in
-              last accu elt.Interface.coq_object_qualid
-	    in
-	    handle_res (List.fold_left fold accu l) k
-	  | _ -> handle_res accu k)
-    in
-    Coq.try_grab coqtop query ignore;
+  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
-  get_semantic (get_aux Proposals.empty buffer#start_iter)
+  Coq.bind (Coq.search flags) next
 
 class undo_manager (buffer : GText.buffer) =
 object(self)
@@ -374,7 +375,7 @@ object (self)
         Minilib.log ("Completion of prefix: '" ^ w ^ "'");
         let (off, prefix, proposals) = last_completion in
         let start_offset = start#offset in
-	let handle_proposals isnew new_proposals k =
+	let handle_proposals isnew new_proposals =
           if isnew then last_completion <- (start_offset, w, new_proposals);
           (* [iter] might be invalid now, get a new one to please gtk *)
           let iter = self#buffer#get_iter `INSERT in
@@ -395,17 +396,23 @@ object (self)
             let sel = self#buffer#get_iter `INSERT in
             self#buffer#select_range sel ins;
             self#buffer#end_user_action ();
-          end;
-	  k ()
+          end
 	in
         (* check whether we have the last request in cache *)
         if (start_offset = off) && (0 <= is_substring prefix w) then
-          handle_proposals false
-	    (Proposals.filter (fun p -> 0 < is_substring w p) proposals)
-	    (fun () -> ())
+          let filter prop = 0 < is_substring w prop in
+          let props = Proposals.filter filter proposals in
+          handle_proposals false props
         else
-	  get_completion self#buffer ct w (handle_proposals true)
-      end
+          (** If not in the cache, we recompute it: first syntactic *)
+          let synt = get_syntactic_completion self#buffer w Proposals.empty in
+          (** Then semantic *)
+          let next accu = Coq.lift (fun () -> handle_proposals true accu) in
+          let query = Coq.bind (get_semantic_completion w synt) next in
+          (** If coqtop is computing, do the syntactic completion altogether *)
+          let occupied () = handle_proposals true synt in
+          Coq.try_grab ct query occupied
+        end
     end
 
   method private may_auto_complete () =