Coqide: get rid of threads, use gtk asynchronous i/o instead

 Threads were only there to handle blocking dialogs with the different
 coqtops. But programming with threads have drawbacks : complex mutex
 infrastructure, possible deadlocks, etc. In particular gtk functions
 are not meant to be called from a thread which isn't the gtk main loop,
 (unless some gtk mutex have been taken). This seem to pose problem
 specifically in win32 (and macosx ?), hence the use of the
 GtkThread.(a)sync hack for scheduling code for execution in the gtk
 main loop.

 Instead, we now use the Glib.Io module to install a callback that will
 be runned when some answer of coqtop is available on the channel.
 This implies using now a continuation-passing style: for instance,
 instead of two sequential requests to coqtop, we'll now have the
 2nd request inside the callback handling the answer to the 1st request.

 Remarks:

 - Also use asynchronous i/o for external commands (editor, coqc, make...).
   Launching an external editor or browser won't freeze coqide anymore.

 - Reworked handling of coqtop process, especially when closing them.
   A responsive coqtop should now hara-kiri immediatly when its input
   channel is closed. Otherwise we try later a soft kill, then some
   hard kills if necessary. If nothing work we warns the user.
   When quitting coqide, all this might induce a small delay (2s at worse).

 - Be careful now to avoid "long" computations (or blocking i/o) in
   a coqide function. Experimentally, it seems that loading/saving a .v
   file is quick enough. If necessary, we could use asynchronous i/o
   also for writing the .v, but for loading I've no clue.

 - In the Coqide module, we ensure that the current continuation k
   will indeed be run at the end thanks to an abstract return type
   (void = opaque copy of unit).

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

1 files changed, 78 insertions, 88 deletions

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 82dd77344..0ab946d65 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -42,7 +42,7 @@ end
 
 module Proposals = Set.Make(StringOrd)
 
-let get_completion (buffer : GText.buffer) coqtop w =
+let get_completion (buffer : GText.buffer) coqtop w handle_res =
   let rec get_aux accu (iter : GText.iter) =
     match iter#forward_search w with
     | None -> accu
@@ -56,23 +56,23 @@ let get_completion (buffer : GText.buffer) coqtop w =
       else get_aux accu stop
   in
   let get_semantic accu =
-    let ans = ref accu in
     let flags = [Interface.Name_Pattern ("^" ^ w), true] in
-    let query handle = match Coq.search handle flags with
-    | 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
-      ans := (List.fold_left fold accu l)
-    | _ -> ()
+    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;
-    !ans
   in
   get_semantic (get_aux Proposals.empty buffer#start_iter)
 
@@ -88,8 +88,6 @@ object (self)
   (* this variable prevents CoqIDE from autocompleting when we have deleted something *)
   val mutable is_auto_completing = false
 
-  val undo_lock = Mutex.create ()
-
   method auto_complete = auto_complete
 
   method set_auto_complete flag =
@@ -142,51 +140,35 @@ object (self)
     self#buffer#insert_interactive ~iter s
 
   method undo () =
-    if Mutex.try_lock undo_lock then begin
-      Minilib.log "UNDO";
-      let effective = self#process_action history in
-      if effective then self#backward ();
-      Mutex.unlock undo_lock;
-      effective
-    end else
-      (Minilib.log "UNDO DISCARDED"; true)
+    Minilib.log "UNDO";
+    let effective = self#process_action history in
+    if effective then self#backward ()
 
   method redo () =
-    if Mutex.try_lock undo_lock then begin
-      Minilib.log "REDO";
-      let effective = self#process_action redo in
-      if effective then self#forward ();
-      Mutex.unlock undo_lock;
-      effective
-    end else
-      (Minilib.log "REDO DISCARDED"; true)
+    Minilib.log "REDO";
+    let effective = self#process_action redo in
+    if effective then self#forward ()
 
   method private handle_insert iter s =
     (* we're inserting, so we may autocomplete *)
     is_auto_completing <- true;
     (* Save the insert action *)
-    if Mutex.try_lock undo_lock then begin
-      let action = Insert (s, iter#offset, Glib.Utf8.length s) in
-      history <- action :: history;
-      redo <- [];
-      self#dump_debug ();
-      Mutex.unlock undo_lock
-    end
+    let action = Insert (s, iter#offset, Glib.Utf8.length s) in
+    history <- action :: history;
+    redo <- [];
+    self#dump_debug ()
 
   method private handle_delete ~start ~stop =
     (* disable autocomplete *)
     is_auto_completing <- false;
     (* Save the delete action *)
-    if Mutex.try_lock undo_lock then begin
-      let start_offset = start#offset in
-      let stop_offset = stop#offset in
-      let s = self#buffer#get_text ~start ~stop () in
-      let action = Delete (s, start_offset, stop_offset - start_offset) in
-      history <- action :: history;
-      redo <- [];
-      self#dump_debug ();
-      Mutex.unlock undo_lock
-    end
+    let start_offset = start#offset in
+    let stop_offset = stop#offset in
+    let s = self#buffer#get_text ~start ~stop () in
+    let action = Delete (s, start_offset, stop_offset - start_offset) in
+    history <- action :: history;
+    redo <- [];
+    self#dump_debug ();
 
   method private do_auto_complete () =
     let iter = self#buffer#get_iter `INSERT in
@@ -197,33 +179,35 @@ object (self)
       if String.length w >= auto_complete_length then begin
         Minilib.log ("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 ct 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)
+	let handle_proposals isnew new_proposals k =
+	  if isnew then last_completion <- (start#offset, w, new_proposals);
+          let prop =
+            try Some (Proposals.choose new_proposals)
+            with Not_found -> None
           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
+          match prop with
+            | None -> k ()
+            | 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;
+	      k ()
+	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 () -> ())
+        else
+	  get_completion self#buffer ct w (handle_proposals true)
       end
     end
 
@@ -340,8 +324,10 @@ object (self)
     (* Install auto-completion *)
     ignore (self#buffer#connect#after#end_user_action ~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()));
+    ignore (self#connect#undo
+	      ~callback:(fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
+    ignore (self#connect#redo
+	      ~callback:(fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));
     (* HACK: Redirect the move_line signal of the underlying GtkSourceView *)
     let move_line_marshal = GtkSignal.marshal2
       Gobject.Data.boolean Gobject.Data.int "move_line_marshal"
@@ -360,9 +346,11 @@ object (self)
       (* do we forward the signal? *)
       let proceed =
         if not b && i = 1 then
-          iter#editable true && iter#forward_line#editable true
+          iter#editable ~default:true &&
+	  iter#forward_line#editable ~default:true
         else if not b && i = -1 then
-          iter#editable true && iter#backward_line#editable true
+          iter#editable ~default:true &&
+	  iter#backward_line#editable ~default:true
         else false
       in
       if not proceed then GtkSignal.stop_emit ()
@@ -376,11 +364,13 @@ let script_view ct ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spa
   GtkSourceView2.SourceView.make_params [] ~cont:(
     GtkText.View.make_params ~cont:(
       GContainer.pack_container ~create:
-	(fun pl -> let w = match source_buffer with
-	  | None -> GtkSourceView2.SourceView.new_ ()
-	  | Some buf -> GtkSourceView2.SourceView.new_with_buffer
-            (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in
-          let w = Gobject.unsafe_cast w in
-		   Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
-		   Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
-		   ((new script_view w ct) : script_view))))
+	(fun pl ->
+	  let w = match source_buffer with
+	    | None -> GtkSourceView2.SourceView.new_ ()
+	    | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+              (Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
+	  in
+	  let w = Gobject.unsafe_cast w in
+	  Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
+	  Gaux.may ~f:(GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+	  ((new script_view w ct) : script_view))))