aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-28 00:06:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-28 00:06:21 +0200
commitdf1d4dc9c3808a811111e4cd9eeda328b51f20de (patch)
tree5afff9b53e69fdfb72de3ae4cc577b330f748bd2 /ide
parent7535e268f7706d1dee263fdbafadf920349103db (diff)
[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
Diffstat (limited to 'ide')
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/wg_ProofView.ml22
-rw-r--r--ide/wg_ProofView.mli2
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