Merge branch 'v8.5'

10 files changed, 137 insertions, 106 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 0fe316b56..fa0adf979 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -460,10 +460,6 @@ let close_coqtop coqtop =
 
 let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop
 
-let break_coqtop coqtop =
-  try !interrupter (CoqTop.unixpid coqtop.handle.proc)
-  with _ -> Minilib.log "Error while sending Ctrl-C"
-
 let get_arguments coqtop = coqtop.sup_args
 
 let set_arguments coqtop args =
@@ -513,6 +509,17 @@ let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
 let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
 
+let break_coqtop coqtop workers =
+  if coqtop.status = Busy then
+    try !interrupter (CoqTop.unixpid coqtop.handle.proc)
+    with _ -> Minilib.log "Error while sending Ctrl-C"
+  else
+    let rec aux = function
+    | [] -> Void
+    | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws)
+    in
+      let Void = aux workers in ()
+
 module PrintOpt =
 struct
   type t = string list
diff --git a/ide/coq.mli b/ide/coq.mli
index d9eda0f34..7cef6a4d0 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
 
-val break_coqtop : coqtop -> unit
-(** Interrupt the current computation of coqtop. *)
+val break_coqtop : coqtop -> string list -> unit
+(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *)
 
 val close_coqtop : coqtop -> unit
 (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 9f36c4e36..6200f1490 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -174,6 +174,55 @@ let validate s =
 
 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)
@@ -206,20 +255,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
@@ -235,8 +272,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/coqide.ml b/ide/coqide.ml
index 8a952f260..1fe393d2b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -570,7 +570,7 @@ module Nav = struct
   let restart _ = on_current_term restart
   let interrupt sn =
     Minilib.log "User break received";
-    Coq.break_coqtop sn.coqtop
+    Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data))
   let interrupt = cb_on_current_term interrupt
   let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
diff --git a/ide/document.ml b/ide/document.ml
index bb431e791..62457fe56 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/session.ml b/ide/session.ml
index 058a422b9..cdec392ec 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -16,6 +16,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
@@ -316,6 +317,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_jobpage coqtop coqops : jobpage =
@@ -355,6 +357,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 8f7c79bec..028a1f9de 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 71825d81e..c2799e40b 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -11,53 +11,13 @@ open Preferences
 
 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
@@ -96,7 +56,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 ()
@@ -114,10 +74,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
@@ -128,17 +90,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
@@ -146,14 +114,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
 
@@ -162,11 +122,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