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

1 files changed, 20 insertions, 1 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d25bc1d9..4e63b16fa 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) =