I think that we should drop the GIF directories, to lighten maintenance,
and that we should in place add an ascii version,
https://us.metamath.org/mpeascii/, so that the feature mentioned by Glauco
stay (and be even better).
The ascii pages should not be hard to generate: in the metamath.c function
generating the unicode pages (generated by the command MM> SHOW STATEMENT
*/HTML), there should be a line saying:
"for token in statement {fetch the htmldef of the token and display it}"
which should be changed to:
"display statement".
That is, it displays precisely the statements as displayed on the command
line of MM> , maybe with the added color code, maybe with italic if it's
the same font, but nothing more.
Benoît
On Monday, January 2, 2023 at 8:47:05 PM UTC+1 Glauco 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?
>
--
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/6faeecdd-e42c-4c62-8230-5f8b3492370dn%40googlegroups.com.
