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 chrome).

(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 MHonArc.