Re: [isabelle] Basic IsarToLatex markup completed
On 12/2/2012 11:06 AM, Makarius wrote:
I would call that control symbol \<^mark> to make its logical function
more clear. The rendering engine would merely have to assign it to
some font style + color change, like it does already for \<^sub> in a
hardwired manner. That would have to become a bit more flexible, to
allow etc/symbols changing the behaviour of control symbols.
(This is merely a summary of what I distilled from above, not any
promise that this will come in the next release.)
So I was being overly ambitious to help other people out, not myself.
For myself, all I need is this:
(1) What is now called \<^isub>, you rename to \<^sub>.
(2) What is now called \<^sub>, you rename to \<^mark>.
Item (1) is what you've already implemented in the development version
(so I understand).
Item (2) is merely renaming a control symbol that has been freed up.
I wouldn't need anything special to distinguish between the use of
\<^sub> and \<^mark>. Context would tell me which was being used.
If you were to tell me today that item (2) is what's going to be done,
then I would just start using \<^sub> as my markup command. It would
make the search and replace in my script fairly mindless, which is the
way I like it.
Thanks for the hypothetical gift. I appreciate it, hypothetically.
If inclined, you would also rename what is now \<^sup> to make it a
markup control symbol. The result would be that, effectively, no
commands are being taken away from Isar. If \<^mark> was being used, and
it looked like \<^sub>, that just means that when a THY was being marked
up, it would require more experience from the user.
This archive was generated by a fusion of
Pipermail (Mailman edition) and