Re: [isabelle] Basic IsarToLatex markup completed

On 12/1/2012 4:02 AM, Makarius wrote:
2) They and the character that follows them get ignored, other than the fact that the character gets subscripted or superscripted.

Does that mean...?

First, I now use \<^usub> and \<^usup> as the new, hypothetical commands you will supply in Isar. The "u" is to emphasize "user reserved". It could be that you want your own \<^psub> and \<^psup> "prover reserved" markup commands.

(1) To clarify, "ignore" means that \<^usub><ASCII or Unicode character> will get parsed for correct syntax, then get displayed as a subscripted character (different looking than the use of \<^sub>), but not get used in any way by the prover engine, and not get flagged as an error, no matter where it is in a THY file.

Here, I make a pseudo sales speech. For myself, I don't have to have any of this. I can modify my script to accommodate how I use Isar.

Suppose you gave us three control characters that behave as described by, or similar to, (1): \<^usub>, \<^usup>, and \<^uchar>, where \<^uchar> simply displays the character in a uniquely visible way.

You would then free up every ASCII and Unicode character to be used as a markup tag in a THY.

The markup we're talking about is more general than HTML or LaTeX markup. We could call it "preprocessing markup". It would give the user the ability to use single characters, single subscripted characters, and single superscripted characters as markup tags for any kind of preprocessing they would want to do.

Myself, I would be using a lot of single characters tags, and I don't think I would ever have to use more than two characters to create my delimiters.


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