Re: [isabelle] Basic IsarToLatex markup completed



On Wed, 28 Nov 2012, Gottfried Barrow wrote:

I got the important parts of my IsarToLatex markup language finished/started, and now I'm ready to start using it. The goal is, after all, to prove things, not just mess around with software.

The basic idea of my humble man's WYSIWYG is:

1) Create markup delimiters by subscripting or superscripting select ASCII or \<...> characters,
2) in non-standard ways,
3) that make the symbols smaller and more discrete,
4) but yet you can still recognize them and not confuse them for similar looking characters, even when using a small font.

Interesting what can be done with a few control symbols. It appears to be generally in line with the "markdown" family of tools. Do you have your own implementation somewhere on the web?

I would have never got the idea to make a subscripted ASCII prime. Such things depend a lot on the actual font being used, though.


There's a jEdit screenshot for people who can't or don't want to load the THY.

The screenshot shows some of my markup characters, and I'm using a size 10 font. The spellchecker is underlining some things.

Which spellchecker are you using here? Are you satisfied with it? At some point I would like to wire-up a reasonably good one with Isabelle/jEdit in a way that it knows about the formal vs. informal parts of the text. So it won't hilight the formal option "SAT4J", for example.


As to generating other THY files from a working file like sTs01.thy, such as a THY that ASCII lovers would find acceptable and useful, that's a future possibility, but not to be done if unnecessary. These days, most people don't expect HTML pages to be converted to TXT files.

At some point I would like to see the Isabelle/Isar sources rendered nicely in HTML, based on similar pseudo-markup symbols as you have here, or like a variant of Markdown that is using non-ASCII characters.

Luckily Isabelle has an infinite amount of \<foo> symbols to play with, and they can be assigned to Unicode glyphs on demand.


	Makarius





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