I think it's not worth it to have ascii symbols in title attributes on every character. This will unnecessarily blow up the page size quite considerably. I think Benoit's suggestion of an all-ascii version of the pages is better - I think this is already implemented in one of the alternate verifiers, and it seems like a better overall approach if the purpose is to get expressions which can be copy-pasted into e.g. an mmj2 worksheet or an .mm file compared to a bunch of tiny tooltips.
On Mon, Jan 2, 2023 at 4:53 PM David A. Wheeler <dwhee...@dwheeler.com> wrote: > > > > On Jan 2, 2023, at 2:47 PM, Glauco <glaformetam...@gmail.com> 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/FF0A4BFB-8BAC-4482-83ED-E409B453552F%40dwheeler.com > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu9J-DBCJW8rwjTXvTsRVhem5G2JTVUJ3OZAEr3naKteg%40mail.gmail.com.
