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"
(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
This archive was generated by a fusion of
Pipermail (Mailman edition) and