Re: [isabelle] Basic IsarToLatex markup completed

On 12/1/2012 4:02 AM, Makarius wrote:
On Fri, 30 Nov 2012, Gottfried Barrow wrote:

Here are three things that would make for safer markup:

1) You leave \<^isub> and \<^isup> in Isar.

2) They and the character that follows them get ignored, other than the fact that the character gets subscripted or superscripted.

Does that mean you want to write "foo\<^sub>\<lless>" as identifier?
Or \<^sub>\<lless> anywhere in the Isar outer syntax to be like a blank?

I answer those questions after a few preliminary remarks.

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.
4) The "my\<^sub>'theorem" is a normal Isar identifier with the allowed subscripted prime, \<^sub>', in the name. I will have possibly copied and pasted "my\<^sub>'theorem" into the comment. Plus, if \<^sub>' is formally part of the identifier, then I definitely don't want to use another character in its place, even if its in a comment.

I used the word "ignored" because I got confused a little. I've only been talking about using \<^isub> inside a comment, --"...", where I can already do what I want with it.

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

Having said all that, I specifically answer your two questions to make sure I have.

1) "Does that mean you want to write "foo\<^sub>\<lless>" as identifier?"

No. The rules and available characters for identifiers are fine with me. Part of the reason I want a \<^msub> is because I heavily use \<^isub>' in identifier names, so trying to use \<^isub>'.....\<^isub>' as delimited text can't easily be done. In general I have to be careful about trying to use \<^isub>' to create pairs of delimiters, and ' is a great subscripted character because it's subtle and it's easy to type.

2) "Or \<^sub>\<lless> anywhere in the Isar outer syntax to be like a blank? ".

No. With this simple markup I'm talking about, I don't want anything to be completely hidden. If I decide to use markup, like

    \<^msub>\<lless>a big equation array\<^msub>\<ggreater>,

though I want \<lless> and \<ggreater> to be small, I want to know that they're there, and recognize what they are.

If you have something fancy in mind to give us, that's fine, but my system is simply based on typing characters in a normal way. We need to see what we typed.

In general, the jEdit text view can render "\<^foo>\<bar>" or "\<^foo>a" in almost arbitrary ways that fit on a 1-dimensional line of text. Any affine transformation on the font can be applied. For \<^sub>a the glyph for \<^sub> is made very thin (and in the next release also with 100% transparency) and the "a" is scaled/translated to give a nice subscript (nicer than the official Java subscript style).

One could also change the font family on the spot, for each of the two symbols separately, but this is presently not done.

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.

Basically, even if I could figure out a way to do a lot of preprocessing on the text in a THY before it got to your prover engine, I wouldn't want to do it, unless it performed some great magic, but not I'm a magician in these matters. The only "One" making changes would be you. I just work within the rules.


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