Coqide: Globalization feedback (proof of concept)

A new feedback message for globalization infos can be sent by
Coq to Coqide.  Coqide stores the information in the proof of
concept module wg_Tooltip, that also sets things up so that
these infos are displayed as a tooltip when the mouse is over
the text they are attached to.  These infos are available only
on locked text, and on the text just processed in the case of an
error (on this piece of text, they vanish as the error tag vanishes
as soon as the user edits the text).

wg_Tooltip stocks these infos as lazy string.  This is not needed
in the proof of concept, but is necessary to scale up:  Coq may not
generate the full piece of info when the message is sent (because of
high computational cost or big size) and just send an id; later on,
when/if the user asks for the piece of info, the gui requests the
info explicitly using the id.

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

10 files changed, 143 insertions, 6 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index d136833d00..15ca34b2fa 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -79,7 +79,8 @@ object(self)
   val cmd_stack = Stack.create ()
 
   initializer
-    Coq.set_feedback_handler _ct self#process_feedback
+    Coq.set_feedback_handler _ct self#process_feedback;
+    Wg_Tooltip.set_tooltip_callback (script :> GText.view)
 
   method private get_start_of_input =
     buffer#get_iter_at_mark (`NAME "start_of_input")
@@ -165,6 +166,18 @@ object(self)
       else Tags.Script.processed in
     buffer#apply_tag tag ~start ~stop
 
+  method private attach_tooltip sentence loc text =
+    let pre_chars, post_chars = Loc.unloc loc in
+    let start_sentence = buffer#get_iter_at_mark sentence.start in
+    let stop_sentence = buffer#get_iter_at_mark sentence.stop in
+    let phrase = start_sentence#get_slice ~stop:stop_sentence in
+    let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
+    let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
+    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
+
   method private process_feedback msg =
     let id = msg.Interface.edit_id in
     if id = 0 || Stack.is_empty cmd_stack then () else
@@ -176,8 +189,14 @@ object(self)
         set_flags sentence (CList.add_set `UNSAFE sentence.flags);
         self#mark_as_needed sentence
     | Interface.Processed, Some sentence -> self#mark_as_needed sentence
-    | _, None -> Minilib.log "Coqide/Coq is really asynchronous now!"
-         (* In this case we shoud look for (exec_)id into cmd_stack *)
+    | Interface.GlobRef(loc, filepath, modpath, ident, ty), Some sentence ->
+        self#attach_tooltip sentence loc
+          (Printf.sprintf "%s %s %s" filepath ident ty)
+    | _ ->
+        if sentence = None then
+          Minilib.log "Coqide/Coq is really asynchronous now!"
+          (* In this case we shoud look for (exec_)id into cmd_stack *)
+        else Minilib.log "Unsupported feedback message"
 
   method private commit_queue_transaction sentence =
     (* A queued command has been successfully done, we push it to [cmd_stack].
@@ -312,6 +331,7 @@ object(self)
       let stop = buffer#get_iter_at_mark stop_mark in
       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#move_mark ~where:start (`NAME "start_of_input");
       buffer#delete_mark start_mark;
       buffer#delete_mark stop_mark
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 45627ea261..fde206732a 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -19,6 +19,7 @@ Coq
 Coq_lex
 Sentence
 Gtk_parsing
+Wg_Tooltip
 Wg_ProofView
 Wg_MessageView
 Wg_Find
diff --git a/ide/session.ml b/ide/session.ml
index 4e95fefca3..46780b2757 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -101,7 +101,8 @@ let set_buffer_handlers buffer script =
     let () = buffer#move_mark (`NAME "prev_insert") ~where in
     let start = get_start () in
     let stop = buffer#end_iter in
-    buffer#remove_tag Tags.Script.error ~start ~stop
+    buffer#remove_tag Tags.Script.error ~start ~stop;
+    buffer#remove_tag Tags.Script.tooltip ~start ~stop
   in
   let end_action_cb () =
     let start = get_start () in
diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml
new file mode 100644
index 0000000000..f85792a4ef
--- /dev/null
+++ b/ide/wg_Tooltip.ml
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  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 =
+    CList.map_filter (fun (i,c) -> if in_interval x i then Some c else None) !l
+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
+      view#misc#set_tooltip_text
+        (String.concat "\n"
+          (CList.uniquize (List.map Lazy.force ss)))
+    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
new file mode 100644
index 0000000000..756814dc9b
--- /dev/null
+++ b/ide/wg_Tooltip.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d25bc1d9c..4e63b16fa7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -670,8 +670,27 @@ let check_no_explicitation l =
   | (_, Some (loc, _)) :: _ ->
     user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
 
+(* This code is taken from dumpglob, and should be shared with it *)
+let feedback_global loc ref =
+  if !Flags.ide_slave then
+    let remove_sections dir =
+      if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+        Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
+      else
+        dir in
+    let sp = Nametab.path_of_global ref in
+    let lib_dp = Lib.library_part ref in
+    let ty = "" in
+    let mod_dp,id = Libnames.repr_path sp in
+    let mod_dp = remove_sections mod_dp in
+    let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+    let filepath = Names.DirPath.to_string lib_dp in
+    let modpath = Names.DirPath.to_string mod_dp_trunc in
+    let ident = Names.Id.to_string id in
+    Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty))
+
 let dump_extended_global loc = function
-  | TrueGlobal ref -> Dumpglob.add_glob loc ref
+  | TrueGlobal ref -> feedback_global loc ref; Dumpglob.add_glob loc ref
   | SynDef sp -> Dumpglob.add_glob_kn loc sp
 
 let intern_extended_global_of_qualid (loc,qid) =
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9667df31c4..a9b596b99e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,6 +15,7 @@ CList
 CString
 CArray
 Util
+Loc
 Serialize
 Xml_utils
 Flags
diff --git a/lib/interface.mli b/lib/interface.mli
index 3ff05f6f2e..e1419da9bf 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -123,6 +123,7 @@ type edit_id = int
 type feedback_content =
   | AddedAxiom
   | Processed
+  | GlobRef of Loc.t * string * string * string * string
 
 type feedback = {
   edit_id : edit_id;
diff --git a/lib/lib.mllib b/lib/lib.mllib
index eb7285bdda..eabac2cfd8 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Xml_lexer
 Xml_parser
-Loc
 Errors
 Bigint
 Dyn
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 823f4245d5..186c3dc890 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -525,15 +525,42 @@ let is_message = function
 | Element ("message", _, _) -> true
 | _ -> false
 
+let of_loc loc =
+  let start, stop = Loc.unloc loc in
+  Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+
+let to_loc xml = match xml with
+| Element ("loc", l,[]) ->
+    (try
+      let start = List.assoc "start" l in
+      let stop = List.assoc "stop" l in
+      Loc.make_loc (int_of_string start, int_of_string stop)
+    with Not_found | Invalid_argument _ -> raise Marshal_error)
+| _ -> raise Marshal_error
+
 let to_feedback_content xml = do_match xml "feedback_content"
   (fun s args -> match s with
   | "addedaxiom" -> AddedAxiom
   | "processed" -> Processed
+  | "globref" ->
+       (match args with
+       | [loc; filepath; modpath; ident; ty] ->
+            GlobRef(to_loc loc, to_string filepath, to_string modpath,
+                    to_string ident, to_string ty)
+       | _ -> raise Marshal_error)
   | _ -> raise Marshal_error)
 
 let of_feedback_content = function
 | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
 | Processed -> constructor "feedback_content" "processed" []
+| GlobRef(loc, filepath, modpath, ident, ty) ->
+    constructor "feedback_content" "globref" [
+      of_loc loc;
+      of_string filepath;
+      of_string modpath;
+      of_string ident;
+      of_string ty
+    ]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in