> On Jan 2, 2023, at 2:47 PM, Glauco <[email protected]> wrote:
>
> The gif version has a useful feature: when you hover on a symbol, the ascii
> string for the symbol is shown.
>
> Would it be possible to have the same behavior in the Unicode version?
Yes. Any HTML element can have a "global attribute", and one of them is "title":
https://www.w3.org/TR/2016/REC-html51-20161101/dom.html#the-title-attribute
If we create a span and use a "title" element we could do the same thing.
I tried out both Firefox and Chrome (on MacOS) and after having for just a
moment I saw the tooltip.
My demo HTML is below, in case anyone else wants to try the experiment.
--- David A. Wheeler
=======
<html>
<body>
<p>
This is a tooltip demo for althtmldef "->" as " → ";
<p>
A<span title="->"> → </span>B.
</body>
</html>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/FF0A4BFB-8BAC-4482-83ED-E409B453552F%40dwheeler.com.
