Implementing a segment-viewer in CoqIDE.

This allows a nifty display of the current state of the document through
a dedicated progress bar.

Also closes bug #3764.

9 files changed, 267 insertions, 12 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index a62cbce73d..d7e2a13cd8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -23,6 +23,12 @@ let str_of_flag = function
   | `ERROR _ -> "E"
   | `INCOMPLETE -> "I"
 
+class type signals =
+object
+  inherit GUtil.ml_signals
+  method changed : callback:(int * mem_flag list -> unit) -> GtkSignal.id
+end
+
 module SentenceId : sig
 
   type sentence = private {
@@ -31,6 +37,8 @@ module SentenceId : sig
     mutable flags : flag list;
     mutable tooltips : (int * int * string) list;
     edit_id : int;
+    mutable index : int;
+    changed_sig : (int * mem_flag list) GUtil.signal;
   }
 
   val mk_sentence :
@@ -44,6 +52,9 @@ module SentenceId : sig
   val hidden_edit_id : unit -> int
   val find_all_tooltips : sentence -> int -> string list
   val add_tooltip : sentence -> int -> int -> string -> unit
+  val set_index : sentence -> int -> unit
+
+  val connect : sentence -> signals
 
   val dbg_to_string :
     GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds
@@ -56,8 +67,16 @@ end = struct
     mutable flags : flag list;
     mutable tooltips : (int * int * string) list;
     edit_id : int;
+    mutable index : int;
+    changed_sig : (int * mem_flag list) GUtil.signal;
   }
 
+  let connect s : signals =
+    object
+      inherit GUtil.ml_signals [s.changed_sig#disconnect]
+      method changed = s.changed_sig#connect ~after
+    end
+
   let id = ref 0
   let mk_sentence ~start ~stop flags = decr id; {
     start = start;
@@ -65,15 +84,20 @@ end = struct
     flags = flags;
     edit_id = !id;
     tooltips = [];
+    index = -1;
+    changed_sig = new GUtil.signal ();
   }
   let hidden_edit_id () = decr id; !id
 
-  let set_flags s f = s.flags <- f
-  let add_flag s f = s.flags <- CList.add_set (=) f s.flags
+  let changed s =
+    s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags)
+
+  let set_flags s f = s.flags <- f; changed s
+  let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s
   let has_flag s mf =
     List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
   let remove_flag s mf =
-    s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags
+    s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s
   let same_sentence s1 s2 = s1.edit_id = s2.edit_id
   let find_all_tooltips s off =
     CList.map_filter (fun (start,stop,t) ->
@@ -81,6 +105,8 @@ end = struct
     s.tooltips
   let add_tooltip s a b t = s.tooltips <- (a,b,t) :: s.tooltips
 
+  let set_index s i = s.index <- i
+
   let dbg_to_string (b : GText.buffer) focused id s =
     let ellipsize s =
             Str.global_replace (Str.regexp "^[\n ]*") ""
@@ -133,12 +159,21 @@ object
   method destroy : unit -> unit
 end
 
+let flags_to_color f =
+  let of_col c = `NAME (Tags.string_of_color c) in
+  if List.mem `PROCESSING f then `NAME "blue"
+  else if List.mem `ERROR f then `NAME "red"
+  else if List.mem `UNSAFE f then `NAME "orange"
+  else if List.mem `INCOMPLETE f then `NAME "gray"
+  else of_col (Tags.get_processed_color ())
+
 module Doc = Document
 
 class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
   (_mv:Wg_MessageView.message_view)
+  (_sg:Wg_Segment.segment)
   (_ct:Coq.coqtop)
   get_filename =
 object(self)
@@ -146,8 +181,10 @@ object(self)
   val buffer = (_script#source_buffer :> GText.buffer)
   val proof = _pv
   val messages = _mv
+  val segment = _sg
 
   val document : sentence Doc.document = Doc.create ()
+  val mutable document_length = 0
 
   val mutable initial_state = Stateid.initial
 
@@ -163,7 +200,24 @@ object(self)
     Coq.set_feedback_handler _ct self#enqueue_feedback;
     script#misc#set_has_tooltip true;
     ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback);
-    feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback
+    feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
+    let on_changed (i, f) = segment#add i (flags_to_color f) in
+    let on_push s =
+      set_index s document_length;
+      (SentenceId.connect s)#changed on_changed;
+      document_length <- succ document_length;
+      segment#set_length document_length;
+      let flags = List.map mem_flag_of_flag s.flags in
+      segment#add s.index (flags_to_color flags);
+    in
+    let on_pop s =
+      set_index s (-1);
+      document_length <- pred document_length;
+      segment#set_length document_length;
+    in
+    let _ = (Doc.connect document)#pushed on_push in
+    let _ = (Doc.connect document)#popped on_pop in
+    ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
     let x, y = script#window_to_buffer_coords `WIDGET x y in
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index d6854a3c04..008e452d3d 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -37,6 +37,7 @@ class coqops :
   Wg_ScriptView.script_view ->
   Wg_ProofView.proof_view ->
   Wg_MessageView.message_view ->
+  Wg_Segment.segment ->
   coqtop ->
   (unit -> string option) ->
   ops
diff --git a/ide/document.ml b/ide/document.ml
index deb780739b..34fcce1b68 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -13,12 +13,31 @@ let invalid_arg s = raise (Invalid_argument ("Document."^s))
 type 'a sentence = { mutable state_id : Stateid.t option; data : 'a }
 
 type id = Stateid.t
+
+class ['a] signals
+  (pushed : 'a GUtil.signal)
+  (popped : 'a GUtil.signal) =
+object (self)
+  inherit GUtil.ml_signals [pushed#disconnect; popped#disconnect]
+  method pushed = pushed#connect ~after
+  method popped = popped#connect ~after
+end
+
 type 'a document = {
   mutable stack : 'a sentence list;
-  mutable context : ('a sentence list * 'a sentence list) option
+  mutable context : ('a sentence list * 'a sentence list) option;
+  pushed_sig : 'a GUtil.signal;
+  popped_sig : 'a GUtil.signal;
+}
+
+let connect d = new signals d.pushed_sig d.popped_sig
+
+let create () = {
+  stack = [];
+  context = None;
+  pushed_sig = new GUtil.signal ();
+  popped_sig = new GUtil.signal ();
 }
-  
-let create () = { stack = []; context = None }
 
 (* Invariant, only the tip is a allowed to have state_id = None *)
 let invariant l = l = [] || (List.hd l).state_id <> None
@@ -34,11 +53,12 @@ let tip_data = function
 
 let push d x =
   assert(invariant d.stack);
-  d.stack <- { data = x; state_id = None } :: d.stack
+  d.stack <- { data = x; state_id = None } :: d.stack;
+  d.pushed_sig#call x
 
 let pop = function
   | { stack = [] } -> raise Empty
-  | { stack = { data }::xs } as s -> s.stack <- xs; data
+  | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data
   
 let focus d ~cond_top:c_start ~cond_bot:c_stop =
   assert(invariant d.stack);
@@ -106,8 +126,6 @@ let is_in_focus d id =
   let _, focused, _ = to_lists d in
   List.exists (fun { state_id } -> stateid_opt_equal state_id (Some id)) focused
 
-let clear d = d.stack <- []; d.context <- None
-  
 let print d f =
   let top, mid, bot = to_lists d in
   let open Pp in
diff --git a/ide/document.mli b/ide/document.mli
index 556e1d0227..8196c0f219 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -104,3 +104,15 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list
 val print :
   'a document -> (bool -> id option -> 'a ->  Pp.std_ppcmds) -> Pp.std_ppcmds
 
+(** Callbacks on documents *)
+
+class ['a] signals :
+  'a GUtil.signal ->
+  'a GUtil.signal ->
+  object
+    inherit GUtil.ml_signals
+    method popped : callback:('a -> unit) -> GtkSignal.id
+    method pushed : callback:('a -> unit) -> GtkSignal.id
+  end
+
+val connect : 'a document -> 'a signals
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 9444761716..e082bd18c1 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,6 +9,7 @@ Configwin
 Editable_cells
 Config_parser
 Tags
+Wg_Segment
 Wg_Notebook
 Config_lexer
 Utf8_convert
diff --git a/ide/session.ml b/ide/session.ml
index 4835307ec5..ecf9a8f8b7 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -33,6 +33,7 @@ type session = {
   script : Wg_ScriptView.script_view;
   proof : Wg_ProofView.proof_view;
   messages : Wg_MessageView.message_view;
+  segment : Wg_Segment.segment;
   fileops : FileOps.ops;
   coqops : CoqOps.ops;
   coqtop : Coq.coqtop;
@@ -368,12 +369,13 @@ let create file coqtop_args =
   let script = create_script coqtop buffer in
   let proof = create_proof () in
   let messages = create_messages () in
+  let segment = new Wg_Segment.segment () in
   let command = new Wg_Command.command_window basename coqtop in
   let finder = new Wg_Find.finder basename (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in
   let cops =
-    new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
+    new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in
   let errpage = create_errpage script in
   let jobpage = create_jobpage coqtop cops in
   let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
@@ -384,6 +386,7 @@ let create file coqtop_args =
     script=script;
     proof=proof;
     messages=messages;
+    segment=segment;
     fileops=fops;
     coqops=cops;
     coqtop=coqtop;
@@ -489,6 +492,7 @@ let build_layout (sn:session) =
 	 end)
   in
   session_box#pack sn.finder#coerce;
+  session_box#pack sn.segment#coerce;
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
diff --git a/ide/session.mli b/ide/session.mli
index 90138a0c98..7949112b36 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -29,6 +29,7 @@ type session = {
   script : Wg_ScriptView.script_view;
   proof : Wg_ProofView.proof_view;
   messages : Wg_MessageView.message_view;
+  segment : Wg_Segment.segment;
   fileops : FileOps.ops;
   coqops : CoqOps.ops;
   coqtop : Coq.coqtop;
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
new file mode 100644
index 0000000000..c9d538a8e4
--- /dev/null
+++ b/ide/wg_Segment.ml
@@ -0,0 +1,143 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+
+type color = GDraw.color
+
+module Segment :
+sig
+  type +'a t
+  val length : 'a t -> int
+  val resize : 'a t -> int -> 'a t
+  val empty : 'a t
+  val add : int -> 'a -> 'a t -> 'a t
+  val remove : int -> 'a t -> 'a t
+  val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+end =
+struct
+  type 'a t = {
+    length : int;
+    content : 'a Int.Map.t;
+  }
+
+  let empty = { length = 0; content = Int.Map.empty }
+
+  let length s = s.length
+
+  let resize s len =
+    if s.length <= len then { s with length = len }
+    else
+      let filter i v = i < len in
+      { length = len; content = Int.Map.filter filter s.content }
+
+  let add i v s =
+    if i < s.length then
+      { s with content = Int.Map.add i v s.content }
+    else s
+
+  let remove i s = { s with content = Int.Map.remove i s.content }
+
+  let fold eq f s accu =
+    let make k v (cur, accu) = match cur with
+    | None -> Some (k, k, v), accu
+    | Some (i, j, w) ->
+      if k = j + 1 && eq v w then Some (i, k, w), accu
+      else Some (k, k, v), (i, j, w) :: accu
+    in
+    let p, segments = Int.Map.fold make s.content (None, []) in
+    let segments = match p with
+    | None -> segments
+    | Some p -> p :: segments
+    in
+    List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments
+
+end
+
+let i2f = float_of_int
+let f2i = int_of_float
+
+let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
+| `BLACK, `BLACK -> true
+| `COLOR c1, `COLOR c2 -> c1 == c2
+| `NAME s1, `NAME s2 -> String.equal s1 s2
+| `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
+| `WHITE, `WHITE -> true
+| _ -> false
+
+class segment () =
+let box = GBin.frame () in
+let draw = GMisc.image ~packing:box#add () in
+object (self)
+
+  inherit GObj.widget box#as_widget
+
+  val mutable width = 1
+  val mutable height = 20
+  val mutable data = Segment.empty
+  val mutable default : color = `WHITE
+  val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
+
+  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
+    in
+    let _ = box#misc#connect#size_allocate cb in
+    (** Initial pixmap *)
+    draw#set_pixmap pixmap
+
+  method length = Segment.length data
+
+  method set_length len =
+    data <- Segment.resize data len;
+    if self#misc#visible then self#refresh ()
+
+  method private fill_range color i j =
+    let i = i2f i in
+    let j = i2f j in
+    let width = i2f width in
+    let len = i2f (Segment.length data) in
+    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;
+
+  method add i color =
+    data <- Segment.add i color data;
+    if self#misc#visible then self#fill_range color i (i + 1)
+
+  method remove i =
+    data <- Segment.remove i data;
+    if self#misc#visible then self#fill_range default i (i + 1)
+
+  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 () =
+    pixmap#set_foreground default;
+    pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
+    let fold i j v () = self#fill_range v i (j + 1) in
+    Segment.fold color_eq fold data ();
+    draw#set_mask None;
+
+end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
new file mode 100644
index 0000000000..cea6058b45
--- /dev/null
+++ b/ide/wg_Segment.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type color = GDraw.color
+
+class segment : unit ->
+  object
+    inherit GObj.widget
+    val obj : Gtk.widget Gtk.obj
+    method length : int
+    method set_length : int -> unit
+    method default_color : color
+    method set_default_color : color -> unit
+    method add : int -> color -> unit
+    method remove : int -> unit
+  end