Re: [isabelle] syntax highlighting on stackoverflow
On Fri, 15 Mar 2013, Christian Sternagel wrote:
The main choices I see are plain ASCII (which would not be very
convenient, since this usually means that you manually have to change
your snippet from using Unicode tokens to plain ASCII before publishing
it; or something like 'isabelle unsymbolize' could be used... but it
would have to cover all "standard" symbols) or some variant of Unicode
(which works for me on Linux with firefox, but e.g. not on Android with
(I am still lagging behind with this thread ...)
The ASCII-fallback approach is basically what we did around 1995, when the
mathematical symbols were working only in exceptional situations.
I am not a fan of Unicode at all, but I have been trying hard for many
years to make it somehow work as front-end display mechanism, hoping that
we can give up ASCII alternatives and "unsymbolize" eventually. I even
composed the IsabelleText font for that, although it has required a few
more years than anticipatated to become usable. (The STIX project did not
reach a usable result in the double time.)
There should be some ways to convince hosting software like the one of
Stackoverflow / Stackexchange to go beyond ASCII.
Another question: if one only sees funny symbols instead of the "real
thing" does this also mean that copy'n'paste won't work in general, or
is this independent from what is visible?
Copy-paste works more often than having things visible. The former is
about encodings, which normally work unless the web server is configured
in a bad way. The latter is about fonts, which often do not work.
HTML5 also allows to specify server-side fonts for local display. So one
could in principle force IsabelleText on the user even on the Web, but
this is still a very theoretic possibility.
This archive was generated by a fusion of
Pipermail (Mailman edition) and