diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:10:02 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:10:02 +0000 |
| commit | 94ad539b17f1509540517ccdedefcda7cdd5fd4f (patch) | |
| tree | c716cc2664cd0c771fbe7e887cde39bdd199fc2d /ide/wg_MessageView.mli | |
| parent | 3845c2333df00c75bc2ffaca8bcaaa76fbad1d66 (diff) | |
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
Diffstat (limited to 'ide/wg_MessageView.mli')
0 files changed, 0 insertions, 0 deletions