Fixing bug #4540: CoqIDE bottom progress bar does not update.

5 files changed, 119 insertions, 99 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 89f4e513e..58f5eda62 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -169,6 +169,55 @@ let flags_to_color f =
 
 module Doc = Document
 
+let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
+object (self)
+
+  val mutable cbs = []
+
+  val mutable document_length = 0
+
+  method length = document_length
+
+  method changed ~callback = cbs <- callback :: cbs
+
+  method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu ->
+    let fold accu _ _ s =
+      let flags = List.map mem_flag_of_flag s.flags in
+      f accu (flags_to_color flags)
+    in
+    Doc.fold_all doc accu fold
+
+  method private on_changed (i, f) =
+    let data = (i, flags_to_color f) in
+    List.iter (fun f -> f (`SET data)) cbs
+
+  method private on_push s ctx =
+    let after = match ctx with
+    | None -> []
+    | Some (l, _) -> l
+    in
+    List.iter (fun s -> set_index s (s.index + 1)) after;
+    set_index s (document_length - List.length after);
+    ignore ((SentenceId.connect s)#changed self#on_changed);
+    document_length <- document_length + 1;
+    List.iter (fun f -> f `INSERT) cbs
+
+  method private on_pop s ctx =
+    let () = match ctx with
+    | None -> ()
+    | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l
+    in
+    set_index s (-1);
+    document_length <- document_length - 1;
+    List.iter (fun f -> f `REMOVE) cbs
+
+  initializer
+    let _ = (Doc.connect doc)#pushed self#on_push in
+    let _ = (Doc.connect doc)#popped self#on_pop in
+    ()
+
+end
+
 class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
@@ -201,20 +250,8 @@ object(self)
     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;
-    let on_changed (i, f) = segment#add i (flags_to_color f) in
-    let on_push s =
-      set_index s document_length;
-      ignore ((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 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
@@ -230,8 +267,6 @@ object(self)
       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
     ()
 
diff --git a/ide/document.ml b/ide/document.ml
index 9823e7576..6566ee3f8 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -16,8 +16,8 @@ type id = Stateid.t
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 class ['a] signal () =
@@ -32,14 +32,14 @@ end
 type 'a document = {
   mutable stack : 'a sentence list;
   mutable context : ('a sentence list * 'a sentence list) option;
-  pushed_sig : 'a signal;
-  popped_sig : 'a signal;
+  pushed_sig : ('a * ('a list * 'a list) option) signal;
+  popped_sig : ('a * ('a list * 'a list) option) signal;
 }
 
-let connect d =
+let connect d : 'a signals =
   object
-    method pushed ~callback = d.pushed_sig#connect callback
-    method popped ~callback = d.popped_sig#connect callback
+    method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx)
+    method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx)
   end
 
 let create () = {
@@ -49,6 +49,12 @@ let create () = {
   popped_sig = new signal ();
 }
 
+let repr_context s = match s.context with
+| None -> None
+| Some (cl, cr) ->
+  let map s = s.data in
+  Some (List.map map cl, List.map map cr)
+
 (* Invariant, only the tip is a allowed to have state_id = None *)
 let invariant l = l = [] || (List.hd l).state_id <> None
 
@@ -64,12 +70,13 @@ let tip_data = function
 let push d x =
   assert(invariant d.stack);
   d.stack <- { data = x; state_id = None } :: d.stack;
-  d.pushed_sig#call x
+  d.pushed_sig#call (x, repr_context d)
 
 let pop = function
   | { stack = [] } -> raise Empty
-  | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data
-  
+  | { stack = { data }::xs } as s ->
+    s.stack <- xs; s.popped_sig#call (data, repr_context s); data
+
 let focus d ~cond_top:c_start ~cond_bot:c_stop =
   assert(invariant d.stack);
   if d.context <> None then invalid_arg "focus";
diff --git a/ide/document.mli b/ide/document.mli
index 0d803ff00..fb96cb6d7 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -108,8 +108,8 @@ val print :
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 val connect : 'a document -> 'a signals
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index b4b02a7fa..47fdeb127 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -10,53 +10,13 @@ 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
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
 end
 
 let i2f = float_of_int
@@ -95,7 +55,7 @@ object (self)
 
   val mutable width = 1
   val mutable height = 20
-  val mutable data = Segment.empty
+  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 ()
@@ -113,10 +73,12 @@ object (self)
       end
     in
     let _ = box#misc#connect#size_allocate cb in
-    let clicked_cb ev =
+    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 = Segment.length data in
+      let len = md#length in
       let idx = f2i ((x *. i2f len) /. i2f width) in
       let () = clicked#call idx in
       true
@@ -125,17 +87,23 @@ object (self)
     (** 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 set_model md =
+    model <- Some md;
+    let changed_cb = function
+    | `INSERT | `REMOVE ->
+      if self#misc#visible then self#refresh ()
+    | `SET (i, color) ->
+      if self#misc#visible then self#fill_range color i (i + 1)
+    in
+    md#changed changed_cb
 
-  method private fill_range color i j =
+  method private fill_range color i j = match model with
+  | None -> ()
+  | Some md ->
     let i = i2f i in
     let j = i2f j in
     let width = i2f width in
-    let len = i2f (Segment.length data) in
+    let len = i2f md#length in
     let x = f2i ((i *. width) /. len) in
     let x' = f2i ((j *. width) /. len) in
     let w = x' - x in
@@ -143,14 +111,6 @@ object (self)
     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
 
@@ -159,11 +119,23 @@ object (self)
     draw#set_pixmap pixmap;
     self#refresh ();
 
-  method private refresh () =
+  method private refresh () = match model with
+  | None -> ()
+  | Some md ->
     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 ();
+    let make (k, cur, accu) v = match cur with
+    | None -> pred k, Some (k, k, v), accu
+    | Some (i, j, w) ->
+      if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu
+      else pred k, Some (k, k, v), (i, j, w) :: accu
+    in
+    let _, p, segments = md#fold make (md#length - 1, None, []) in
+    let segments = match p with
+    | 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;
 
   method connect =
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 0fc8ebd75..29cbbedac 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -8,6 +8,8 @@
 
 type color = GDraw.color
 
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
+
 class type segment_signals =
 object
   inherit GObj.misc_signals
@@ -15,15 +17,19 @@ object
   method clicked : callback:(int -> unit) -> GtkSignal.id
 end
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
+end
+
 class segment : unit ->
   object
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
+    method set_model : model -> unit
     method connect : segment_signals
-    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