Re: [isabelle] syntax highlighting on stackoverflow



Dear all,

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

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?

cheers

chris

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?

Greetings,
Joachim

Joachim,

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:

http://math.stackexchange.com/questions/323029/how-to-show-that-vdash-forall-x-beta-to-alpha-leftrightarrow-exists-x/325877#comment705043_325877


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.

http://math.stackexchange.com/posts/323029/edit

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.

Thanks,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.