Merge PR #9807: Fix CoqIDE progress bar.

Reviewed-by: Zimmi48

4 files changed, 32 insertions, 59 deletions

diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 4aa0f04964..f4786d9431 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/2923bd5d0669f1ec6ab03ddce052e9c5efb46d8f.tar.gz";
-  sha256 = "16cn93rpxfql5idhigyjyhc013a3hwzyy2dl1xv7h2p78sk728vw";
+  url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz";
+  sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7";
 })
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 4aa801c2b2..8da9900724 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -250,7 +250,6 @@ object(self)
     feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
     let md = segment_model document in
     segment#set_model md;
-(*
     let on_click id =
       let find _ _ s = Int.equal s.index id in
       let sentence = Doc.find document find in
@@ -267,7 +266,6 @@ object(self)
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
     let _ = segment#connect#clicked ~callback:on_click in
-*)
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 2e5de64254..b62c0a2190 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -8,10 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*
 open Util
 open Preferences
-*)
 
 type color = GDraw.color
 
@@ -24,7 +22,6 @@ object
   method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
 end
 
-(*
 let i2f = float_of_int
 let f2i = int_of_float
 
@@ -35,14 +32,20 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
 | `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
 | `WHITE, `WHITE -> true
 | _ -> false
-*)
+
+let set_cairo_color ctx c =
+  let open Gdk.Color in
+  let c = GDraw.color c in
+  let cast i = i2f i /. 65536. in
+  Cairo.set_source_rgb ctx (cast @@ red c) (cast @@ green c) (cast @@ blue c)
+
 class type segment_signals =
 object
   inherit GObj.misc_signals
   inherit GUtil.add_ml_signals
   method clicked : callback:(int -> unit) -> GtkSignal.id
 end
-(*
+
 class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals =
 object
   val after = false
@@ -50,14 +53,11 @@ object
   inherit GUtil.add_ml_signals obj [clicked#disconnect]
   method clicked = clicked#connect ~after
 end
-*)
 
 class segment () =
 let box = GBin.frame () in
-(*
-let eventbox = GBin.event_box ~packing:box#add () in
-let draw = GMisc.image ~packing:eventbox#add () in
-*)
+let draw = GMisc.drawing_area ~packing:box#add () in
+
 object (self)
 
   inherit GObj.widget box#as_widget
@@ -66,56 +66,40 @@ object (self)
   val mutable height = 20
   val mutable model : model option = None
   val mutable default : color = `WHITE
-(*
-  val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
-*)
   val clicked = new GUtil.signal ()
-  val mutable need_refresh = false
-  val refresh_timer = Ideutils.mktimer ()
-(*
+
   initializer
     box#misc#set_size_request ~height ();
     let cb rect =
       let w = rect.Gtk.width in
       let h = rect.Gtk.height in
-      (* Only refresh when size actually changed, otherwise loops *)
-      if self#misc#visible && (width <> w || height <> h) then begin
-        width <- w;
-        height <- h;
-        self#redraw ();
-      end
+      width <- w;
+      height <- h
     in
     let _ = box#misc#connect#size_allocate ~callback:cb in
+    let () = draw#event#add [`BUTTON_PRESS] in
     let clicked_cb ev = match model with
     | None -> true
     | Some md ->
       let x = GdkEvent.Button.x ev in
-      let (width, _) = pixmap#size in
       let len = md#length in
       let idx = f2i ((x *. i2f len) /. i2f width) in
       let () = clicked#call idx in
       true
     in
-    let _ = eventbox#event#connect#button_press ~callback:clicked_cb in
+    let _ = draw#event#connect#button_press ~callback:clicked_cb in
     let cb show = if show then self#misc#show () else self#misc#hide () in
     stick show_progress_bar self cb;
-    (* Initial pixmap *)
-    draw#set_pixmap pixmap;
-    refresh_timer.Ideutils.run ~ms:300
-      ~callback:(fun () -> if need_refresh then self#refresh (); true)
-*)
+    let cb ctx = self#refresh ctx; false in
+    let _ = draw#misc#connect#draw ~callback:cb in
+    ()
+
   method set_model md =
     model <- Some md;
-    let changed_cb = function
-    | `INSERT | `REMOVE ->
-      if self#misc#visible then need_refresh <- true
-    | `SET (i, color) ->
-      ()
-(*      if self#misc#visible then self#fill_range color i (i + 1)*)
-    in
+    let changed_cb _ = self#misc#queue_draw () in
     md#changed ~callback:changed_cb
-(*
-  method private fill_range color i j = match model with
+
+  method private fill_range ctx color i j = match model with
   | None -> ()
   | Some md ->
     let i = i2f i in
@@ -125,24 +109,19 @@ object (self)
     let x = f2i ((i *. width) /. len) in
     let x' = f2i ((j *. width) /. len) in
     let w = x' - x in
-    pixmap#set_foreground color;
-    pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true ();
-    draw#set_mask None;
+    set_cairo_color ctx color;
+    Cairo.rectangle ctx (i2f x) 0. ~w:(i2f w) ~h:(i2f height);
+    Cairo.fill ctx
 
   method set_default_color color = default <- color
   method default_color = default
 
-  method private redraw () =
-    pixmap <- GDraw.pixmap ~width ~height ();
-    draw#set_pixmap pixmap;
-    self#refresh ();
-
-  method private refresh () = match model with
+  method private refresh ctx = match model with
   | None -> ()
   | Some md ->
-    need_refresh <- false;
-    pixmap#set_foreground default;
-    pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
+    set_cairo_color ctx default;
+    Cairo.rectangle ctx 0. 0. ~w:(i2f width) ~h:(i2f height);
+    Cairo.fill ctx;
     let make (k, cur, accu) v = match cur with
     | None -> pred k, Some (k, k, v), accu
     | Some (i, j, w) ->
@@ -154,11 +133,9 @@ object (self)
     | None -> segments
     | Some p -> p :: segments
     in
-    List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments;
-    draw#set_mask None;
+    List.iter (fun (i, j, v) -> self#fill_range ctx v i (j + 1)) segments
 
   method connect =
     new segment_signals_impl box#as_widget clicked
-*)
 
 end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 84d487f35f..07f545fee7 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -31,9 +31,7 @@ class segment : unit ->
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
     method set_model : model -> unit
-(*
     method connect : segment_signals
     method default_color : color
     method set_default_color : color -> unit
-*)
   end