Re: [isabelle] syntax highlighting on stackoverflow
Just some general remarks on the format of theory-snippets on
stackoverflow (and in principle also all other possible occurrences). In
my opinion it should be:
- copy'n'paste-able to and fro jEdit (for creation and afterwards)
- human readable (without effort, i.e., nothing like \<subseteq>)
I think that already excludes LaTeX, or not? (Besides, creating a
snippet using LaTeX is much more cumbersome than just copy'n'paste from
your current theory.)
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
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?
On 03/15/2013 12:40 AM, Gottfried Barrow wrote:
On 3/13/2013 10:55 AM, Joachim Breitner wrote:
It is probably not a question of encoding; The correct encoding
(text/html; charset=utf-8) is transferred in the HTTP header, and things
look good here. Maybe your are missing some fonts, of have some
font-overwrite in place?
That's probably the case, so I at least know where the problem is.
But I'm using Windows 7, and so at this stage of the game, if fonts
across operating systems aren't standardized enough to prevent this kind
of thing, then I don't care to set my system up to be bullet proof,
because all that does is allow me to have the impression that others are
seeing what I see.
Eventually, if possible and I'm thinking right, then I try and adapt to
others, rather than expect others to be just like me.
There is ASCII, LaTeX, images, THY files, and PDF files (where even PDFs
can have font dependency problems). Those are what I can depend on.
Nothing else. So I'm trying to come up with practical ways to use those
to ask questions, and say what I want to say.
Here's another person complaining about the same problem:
If you look at the question that's asked, you see that LaTeX is that
sites solution to the problem of dealing with non-ASCII characters.
LaTeX can be a pain, but at least it's consistent and dependable. So
it's annoying when the admins on stackoveflow tell us that "programmers"
don't need LaTeX. If they don't want to implement it, they're the boss,
but attempts at brainwashing to deflect criticism are to be frowned upon.
This archive was generated by a fusion of
Pipermail (Mailman edition) and