Made the CoqIDE progress gutter clickable.

3 files changed, 47 insertions, 1 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 52e184564..689d4908f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -215,8 +215,17 @@ object(self)
       document_length <- pred document_length;
       segment#set_length document_length;
     in
+    let on_click id =
+      let find _ _ s = Int.equal s.index id in
+      let sentence = Doc.find document find in
+      let mark = sentence.stop in
+      let iter = script#buffer#get_iter_at_mark mark in
+      script#buffer#place_cursor iter;
+      ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
+    in
     let _ = (Doc.connect document)#pushed on_push in
     let _ = (Doc.connect document)#popped on_pop in
+    let _ = segment#connect#clicked on_click in
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 8520727a7..25a031d6e 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -70,9 +70,25 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
 | `WHITE, `WHITE -> true
 | _ -> false
 
+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
+  inherit GObj.misc_signals obj
+  inherit GUtil.add_ml_signals obj [clicked#disconnect]
+  method clicked = clicked#connect ~after
+end
+
 class segment () =
 let box = GBin.frame () in
-let draw = GMisc.image ~packing:box#add () in
+let eventbox = GBin.event_box ~packing:box#add () in
+let draw = GMisc.image ~packing:eventbox#add () in
 object (self)
 
   inherit GObj.widget box#as_widget
@@ -82,6 +98,7 @@ object (self)
   val mutable data = Segment.empty
   val mutable default : color = `WHITE
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
+  val clicked = new GUtil.signal ()
 
   initializer
     box#misc#set_size_request ~height ();
@@ -96,6 +113,15 @@ object (self)
       end
     in
     let _ = box#misc#connect#size_allocate cb in
+    let clicked_cb ev =
+      let x = GdkEvent.Button.x ev in
+      let (width, _) = pixmap#size in
+      let len = Segment.length data in
+      let idx = f2i ((x *. i2f len) /. i2f width) in
+      let () = clicked#call idx in
+      true
+    in
+    let _ = eventbox#event#connect#button_press clicked_cb in
     (** Initial pixmap *)
     draw#set_pixmap pixmap
 
@@ -140,4 +166,7 @@ object (self)
     Segment.fold color_eq fold data ();
     draw#set_mask None;
 
+  method connect =
+    new segment_signals_impl box#as_widget clicked
+
 end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index ecb451475..0263856ae 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -8,10 +8,18 @@
 
 type color = GDraw.color
 
+class type segment_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method clicked : callback:(int -> unit) -> GtkSignal.id
+end
+
 class segment : unit ->
   object
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
+    method connect : segment_signals
     method length : int
     method set_length : int -> unit
     method default_color : color