[coqide] Protect against size_allocate race in proofview.

To handle dynamic printing in CoqIDE we listen to the
`size_allocate` signal , [see more details in
6885a398229918865378ea24f07d93d2bcdd2802]

However, we must be careful to protect against scrollbar creation: it
is possible for the `size_allocate` handler to change the size when
inserting text (due to scrollbars), thus we may enter in an infinite
loop.

Our fix is to check if the width has really changed, as done in
`Wg_MessageView`.

This fixes the problem noted by @herbelin in
https://coq.inria.fr/bugs/show_bug.cgi?id=5417

3 files changed, 19 insertions, 7 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 4a1d688f5..45b5a1007 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -358,7 +358,7 @@ object(self)
         | Good evs ->
           proof#set_goals goals;
           proof#set_evars evs;
-          proof#refresh ();
+          proof#refresh ~force:true;
           Coq.return ()
         )
       )
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b5405570c..3cbe58388 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -14,7 +14,7 @@ class type proof_view =
   object
     inherit GObj.widget
     method buffer : GText.buffer
-    method refresh : unit -> unit
+    method refresh : force:bool -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
@@ -197,6 +197,7 @@ let proof_view () =
     inherit GObj.widget view#as_widget
     val mutable goals = None
     val mutable evars = None
+    val mutable last_width = -1
 
     method buffer = text_buffer
 
@@ -206,13 +207,24 @@ let proof_view () =
 
     method set_evars evs = evars <- evs
 
-    method refresh () =
-      let dummy _ () = () in
-      display (mode_tactic dummy) view goals None evars
+    method refresh ~force =
+      (* We need to block updates here due to the following race:
+         insertion of messages may create a vertical scrollbar, this
+         will trigger a width change, calling refresh again and
+         going into an infinite loop. *)
+      let width = Ideutils.textview_width view  in
+      (* Could still this method race if the scrollbar changes the
+         textview_width ?? *)
+      let needed = force || last_width <> width in
+      if needed then begin
+        last_width <- width;
+        let dummy _ () = () in
+        display (mode_tactic dummy) view goals None evars
+      end
   end
   in
   (* Is there a better way to connect the signal ? *)
   (* Can this be done in the object constructor? *)
-  let w_cb _ = pf#refresh () in
+  let w_cb _ = pf#refresh ~force:false in
   ignore (view#misc#connect#size_allocate w_cb);
   pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index aa01d955d..a90d429d0 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -10,7 +10,7 @@ class type proof_view =
   object
     inherit GObj.widget
     method buffer : GText.buffer
-    method refresh : unit -> unit
+    method refresh : force:bool -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit