Re: [isabelle] Basic IsarToLatex markup completed

On Sat, 1 Dec 2012, Gottfried Barrow wrote:

In place of \<^isub>, I'll call what I want \<^msub>, for user-markup subscript. I want to have two different subscript commands, the normal one, \<^sub> (which you've said will be the only one), and this new command \<^msub>.

I want to write something like this:

--"\<^msub>' Please consider the equation \<^msub>'x+1\<^msub>' in theorem \<^msub>*my\<^sub>'theorem\<^msub>*."

This above is an Isar comment that will become normal LaTeX text, that is, text in a text{*...*}.

1) The --"\<^msub>'..." marks it as normal LaTeX text that's outside of any other environment.
2) The \<^msub>'....\<^msub>' is a math inline equation.
3) The \<^msub*.....\<^msub>* is typewriter font.

I'll expand on describing these new commands, \<^msub> and \<^msup>.

1) They are reserved for user's use. A user can interpret a \<^msub> or \<^msup> subscripted or superscripted character any way they want. 2) They hide nothing. They subscript or superscript the character that follows them in a reasonably normal manner. 3) The character that they subscript or superscript is distinguishable from characters subscripted and superscripted with \<^sub> and \<^sup>.

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

4) They can be used anywhere in a THY file.

Item 4 would be where you would sometimes need to "ignore" a \<^msub> or \<^msup>, and the character after them.

I haven't even been wanting to markup anything outside of a --"..." comment, but I throw out item 4 to make the use of \<^msub> and \<^msup> as general as possible.

When it is not required there is no point to think about it too much.

Assigning phyisical rendering to control symbols is one thing, but specifying a certain meaning as part of the syntax is another. The latter is usually avoided, and the etc/symbols file does not cover that at all. E.g. you can't say that something should be a "letter", "digit", "blank" that was not known as such before.

This brings up a restatement of one of my rules, which would be, "The THY can only be edited in a way which conforms to the rules".

I can do all the preprocessing I want on a THY before I feed it to LaTeX, but if someone wants to open up one of my THYs, then I want them to see what I have been seeing, and I don't them to get any errors.

Inventing Isabelle symbols that are not used elsewhere is perfectly within the rules of the free-form typesetting of Isabelle documents. You can have your scripts to post-process the symbols in the "text" ranges, and people have done that before. It merely needs an awarenes that you don't "declare" use of special symbols formally, so there is always a potential to clash with other people's scripts and tools. But this is the same in regular LaTeX.


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