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/coq.ml | |
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/coq.ml')
0 files changed, 0 insertions, 0 deletions