From 637e200e44c6144d0ec8ac28867ec2c5484ffc2d Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 25 Apr 2013 14:14:42 +0000 Subject: 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 --- lib/lib.mllib | 1 - 1 file changed, 1 deletion(-) (limited to 'lib/lib.mllib') diff --git a/lib/lib.mllib b/lib/lib.mllib index eb7285bdd..eabac2cfd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,6 +1,5 @@ Xml_lexer Xml_parser -Loc Errors Bigint Dyn -- cgit v1.2.3