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 MHonArc.