CoqIDE: wg_Tooltip removed, new tooltip handling

- tooltips are attached to sentences
- to find the tooltip text one goes back
  until the first start of sentence mark,
  finds the corresponding sentence and
  displays the tooltip
- focused editing does not invalidate tooltips this way,
  since the text, its tags and marks is moved around consistently

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 48 insertions, 78 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1deb0a8ba..92b2a5e74 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -28,6 +28,7 @@ module SentenceId : sig
     start : GText.mark;
     stop : GText.mark;
     mutable flags : flag list;
+    mutable tooltips : (int * int * string lazy_t) list;
     edit_id : int;
     mutable state_id : Stateid.t option;
   }
@@ -42,6 +43,8 @@ module SentenceId : sig
   val remove_flag : sentence -> mem_flag -> unit
   val same_sentence : sentence -> sentence -> bool
   val hidden_edit_id : unit -> int
+  val find_all_tooltips : sentence -> int -> string lazy_t list
+  val add_tooltip : sentence -> int -> int -> string lazy_t -> unit
 
   val dbg_to_string : GText.buffer -> sentence -> string
 
@@ -51,6 +54,7 @@ end = struct
     start : GText.mark;
     stop : GText.mark;
     mutable flags : flag list;
+    mutable tooltips : (int * int * string lazy_t) list;
     edit_id : int;
     mutable state_id : Stateid.t option;
   }
@@ -62,6 +66,7 @@ end = struct
     flags = flags;
     edit_id = !id;
     state_id = None;
+    tooltips = [];
   }
   let hidden_edit_id () = decr id; !id
 
@@ -76,13 +81,18 @@ end = struct
   let remove_flag s mf =
     s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags
   let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id
+  let find_all_tooltips s off =
+    CList.map_filter (fun (start,stop,t) ->
+      if start <= off && off <= stop then Some t else None)
+    s.tooltips
+  let add_tooltip s a b t = s.tooltips <- (a,b,t) :: s.tooltips
 
   let dbg_to_string (b : GText.buffer) s =
     let ellipsize s =
             Str.global_replace (Str.regexp "^[\n ]*") ""
         (if String.length s > 20 then String.sub s 0 17 ^ "..."
          else s) in
-    Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s]"
+    Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s] %s"
       s.edit_id
       (Stateid.to_string (Option.default Stateid.dummy s.state_id))
       (b#get_iter_at_mark s.start)#offset
@@ -90,6 +100,10 @@ end = struct
       (ellipsize
         ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
       (String.concat "," (List.map str_of_flag s.flags))
+      (ellipsize
+        (String.concat ","
+          (List.map (fun (a,b,t) ->
+             Printf.sprintf "<%d,%d> %s" a b (Lazy.force t)) s.tooltips)))
 
 
 end
@@ -148,9 +162,37 @@ object(self)
 
   initializer
     Coq.set_feedback_handler _ct self#enqueue_feedback;
-    Wg_Tooltip.set_tooltip_callback (script :> GText.view);
+    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
 
+  method private tooltip_callback ~x ~y ~kbd tooltip =
+    let x, y = script#window_to_buffer_coords `WIDGET x y in
+    let iter = script#get_iter_at_location x y in
+    if iter#has_tag Tags.Script.tooltip then begin
+      let s =
+        let rec aux iter =
+          let marks = iter#marks in
+          if marks = [] then aux iter#backward_char
+          else
+            let mem_marks s =
+              List.exists (fun m ->
+                Gobject.get_oid m =
+                Gobject.get_oid (buffer#get_mark s.start)) marks in
+            try Stack.find mem_marks cmd_stack
+            with Not_found -> aux iter#backward_char in
+        aux iter in
+      let ss =
+        find_all_tooltips s
+          (iter#offset - (buffer#get_iter_at_mark s.start)#offset) in
+      let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in
+      GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON;
+      script#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>")
+    end else begin
+      script#misc#set_tooltip_text ""; script#misc#set_has_tooltip true
+    end;
+    false
+    
   method destroy () =
     feedback_timer.Ideutils.kill ()
 
@@ -266,7 +308,9 @@ object(self)
     let start = start_sentence#forward_chars pre in
     let stop = start_sentence#forward_chars post in
     let markup = lazy text in
-    Wg_Tooltip.apply_tooltip_tag buffer ~start ~stop ~markup
+    buffer#apply_tag Tags.Script.tooltip ~start ~stop;
+    add_tooltip sentence pre post markup;
+    self#print_stack
 
   method private is_dummy_id id =
     match id with
@@ -549,7 +593,7 @@ object(self)
         " "^string_of_int stop#offset);
       buffer#remove_tag Tags.Script.processed ~start ~stop;
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-(*       buffer#remove_tag Tags.Script.tooltip ~start ~stop; *)
+      buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 81e36763e..ce4fcca0d 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -19,7 +19,6 @@ Coq
 Coq_lex
 Sentence
 Gtk_parsing
-Wg_Tooltip
 Wg_ProofView
 Wg_MessageView
 Wg_Find
diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml
deleted file mode 100644
index 62598dd50..000000000
--- a/ide/wg_Tooltip.ml
+++ /dev/null
@@ -1,59 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(* This super inefficient thing should be an interval tree *)
-module Table = struct
-  type 'a t = ((int * int) * 'a) list ref
-
-  let in_interval x (i1,i2) = i1 - x <= 0 && i2 - x > 0
-  let overlap_interval (i1,i2 as x) (j1,j2 as y) =
-    in_interval i1 y || in_interval i2 y || in_interval j1 x
-
-  let create () = ref []
-  let add l i c = l := (i,c) :: !l
-  let remove_all l i =
-    l := List.filter (fun (j,_) -> not (overlap_interval i j)) !l
-  let find_all l x =
-    let res =
-      CList.map_filter
-        (fun (i,c) -> if in_interval x i then Some c else None)
-        !l
-    in
-    if res = [] then raise Not_found else res
-end
-
-let table : string lazy_t Table.t = Table.create ()
-
-let tooltip_callback (view : GText.view) ~x ~y ~kbd tooltip =
-  let x, y = view#window_to_buffer_coords `WIDGET x y in
-  let iter = view#get_iter_at_location x y in
-  if iter#has_tag Tags.Script.tooltip then begin
-    try
-      let ss = Table.find_all table iter#offset in
-      let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in
-      GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON;
-      view#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>")
-    with Not_found -> ()
-  end else begin
-    view#misc#set_tooltip_text ""; view#misc#set_has_tooltip true
-  end;
-  false
-
-let remove_tag_callback tag ~start ~stop =
-  if tag#get_oid = Tags.Script.tooltip#get_oid then
-    Table.remove_all table (start#offset,stop#offset) 
-
-let apply_tooltip_tag (buffer : GText.buffer) ~start ~stop ~markup =
-  Table.add table (start#offset,stop#offset) markup;
-  buffer#apply_tag Tags.Script.tooltip ~start ~stop
-
-let set_tooltip_callback view =
-  view#misc#set_has_tooltip true;
-  ignore(view#misc#connect#query_tooltip ~callback:(tooltip_callback view));
-  ignore(view#buffer#connect#remove_tag ~callback:remove_tag_callback)
-
diff --git a/ide/wg_Tooltip.mli b/ide/wg_Tooltip.mli
deleted file mode 100644
index 756814dc9..000000000
--- a/ide/wg_Tooltip.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-val apply_tooltip_tag :
-  GText.buffer ->
-  start:GText.iter -> stop:GText.iter ->
-  markup:string lazy_t -> unit
-
-val set_tooltip_callback : GText.view -> unit