From df1d4dc9c3808a811111e4cd9eeda328b51f20de Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Mar 2017 00:06:21 +0200 Subject: [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 --- ide/wg_ProofView.ml | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) (limited to 'ide/wg_ProofView.ml') 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 -- cgit v1.2.3