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, 2 insertions, 1 deletions

diff --git a/ide/session.ml b/ide/session.ml
index 4e95fefca..46780b275 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