Unicode Tokens: cleanups

[David Aspinall]

Final 4.0 cleanups:

• choice of default fonts: see if can get sensible config (at least for fontconfig platforms) on Emacs 23
• nested regions (fix again)
• customization options (remove from menu for now; add buffer extensibility perhaps)

[David Aspinall]

Some more items:

• Support Coq and PhoX cleanly
• Optimise frequently called functions where possible

[David Aspinall]

Coq support is now good. Still nothing for PhoX.

[Norbert Schirmer]

Super / subscripts are not properly displayed on (Carbon) Emacs 23.3.1. They appear just as normal text. Changing the Script-Font (via the Token menu) has no effect. Is this also on the agenda for Final 4.0?

[Norbert Schirmer]

Script control tokens like \<^bsub>...\<esub> etc. are revealed in locked region.

[Norbert Schirmer]

In Subsequent \<^isub>x\<isub>y only x is displayed properly, whereas the second 'isub' is revealed.

[David Aspinall]

Norbert: thanks for the report about this. It is pretty bad news!

Some quick tests suggest that the display engine is broken on the Mac port (only some versions?), in that it doesn't respond to display raise text properties as it did before in Emacs 22.X (and does on Linux).

Instead of individual characters being affected the whole line is adjusted, which destroys the sub/superscript appearance.

Unfortunately beyond control of PG to fix this.

[Norbert Schirmer]

In the gtk-Version for mac: GNU Emacs 23.1.1 (i386-apple-darwin10.0.0, GTK+ Version 2.14.7) the super / subscripts work fine. The 'raise text' issue seems to be related to the Carbon versions, e.g. GNU Emacs 23.1.1 (i386-apple-darwin10.0.0, NS apple-appkit-1038.11).

[Norbert Schirmer]

With respect to the issue with subsequent isubs, maybe introduce a proper ibsub..iesub region.

[Norbert Schirmer]

Refinement to my comments above:

• subscripts in locked region are revealed the moment you finish a lemma. As long as you work within the lemma it is fine.
• behaviour of subsequent isub's and sub's should be made the same in Isabelle's latex output and PG. Either all the rest of the word is affected or only one letter.

[David Aspinall]

Replying to NorbertSchirmer:

With respect to the issue with subsequent isubs, maybe introduce a proper ibsub..iesub region.

We already have \<^bsub> ... \<^esub> (and I wish Isabelle did not have the single identifier versions). Or did you mean something else?

[David Aspinall]

Replying to NorbertSchirmer:

Refinement to my comments above:

• subscripts in locked region are revealed the moment you finish a lemma. As long as you work within the lemma it is fine.

Can't duplicate this. Can you give an example and say which platform you are using?

• behaviour of subsequent isub's and sub's should be made the same in Isabelle's latex output and PG. Either all the rest of the word is affected or only one letter.

Agreed. Unfortunately there is only one configuration setting in Unicode Tokens at the moment so different prefix behaviour is not possible. TBH I think this is unnecessarily over-complicated in Isabelle. Anyway, which way should it be, can you point me to documentation?

[Norbert Schirmer]

Replying to da:

Replying to NorbertSchirmer:

With respect to the issue with subsequent isubs, maybe introduce a proper ibsub..iesub region.

We already have \<^bsub> ... \<^esub> (and I wish Isabelle did not have the single identifier versions). Or did you mean something else?

However \<^bsub> ... \<^esub> cannot be part of an Isabelle Identifier, but \<^isub> can, thats why it is really different.

[Norbert Schirmer]

Replying to da:

Replying to NorbertSchirmer:

Refinement to my comments above:

• subscripts in locked region are revealed the moment you finish a lemma. As long as you work within the lemma it is fine.

Can't duplicate this. Can you give an example and say which platform you are using?

Mac OS X, 10.6.2; GNU Emacs 23.1.1 (i386-apple-darwin10.0.0, GTK+ Version 2.14.7) example:

lemma

assumes asm: "P\<^{isub>i \<and> Q\<}isub>i" shows "Q\<^{isub>i \<and> P\<}isub>i"

proof -

from asm obtain "P\<^{isub>i" and "Q\<}isub>i"

by blast

then show "Q\<^{isub>i \<and> P\<}isub>i"

by simp

qed

After the qed is processed all the isubs between proof and qed become visible.

• behaviour of subsequent isub's and sub's should be made the same in Isabelle's latex output and PG. Either all the rest of the word is affected or only one letter.

Agreed. Unfortunately there is only one configuration setting in Unicode Tokens at the moment so different prefix behaviour is not possible. TBH I think this is unnecessarily over-complicated in Isabelle. Anyway, which way should it be, can you point me to documentation?

I don't know of documentation, but according to the latex style (isabelle.sty), isub / sub is only affecting a single letter. To subscript more the one letter one has to prefix each one with isub.

[David Aspinall]

Thanks for the example... not sure why I hadn't seen this before, it occurs on Linux too. Repeated and thinking of fix. See #310.

[David Aspinall]

However \<^bsub> ... \<^esub> cannot be part of an Isabelle Identifier, but \<^isub> can, thats why it is really different.

Ah, OK, I had forgotten that. I can't see how you can tell what things should be from isabelle.sty because it depends on how the latex is generated (surrounding arguments with braces or not).

The behaviour in PG is controlled by isar-control-char-format-regexp' in isar-unicode-tokens.el'. It uses `isar-long-id-stuff' inside the regexp which causes the whole word (identifier) to be subscripted. Is that wrong then?

The previous version (commented out) just used a single character but that didn't allow subscripted symbols. Current attempted fix: we now allow subscripted symbols but not subscripted control characters. If long id is wrong, please tell me the right regexp to use here!

[David Aspinall]

With respect to the issue with subsequent isubs, maybe introduce a proper ibsub..iesub region.

P.S., that's trivial to do inside isar-unicode-tokens.el, simply extend isar-control-regions in the obvious way (maybe: bisub, eisub for consistency!). But the Isabelle parser would need to be changed, wouldn't it?

[Norbert Schirmer]

Replying to da:

However \<^bsub> ... \<^esub> cannot be part of an Isabelle Identifier, but \<^isub> can, thats why it is really different.

Ah, OK, I had forgotten that. I can't see how you can tell what things should be from isabelle.sty because it depends on how the latex is generated (surrounding arguments with braces or not).

Currently no braces are generated. That means that latex takes exactly the next letter as an argument, as far as I can tell from the output. To extend this to the whole rest of the identifier we need a real tex expert (as long as we do not have an syntactic marker for the end like eisub).

The behaviour in PG is controlled by isar-control-char-format-regexp' in isar-unicode-tokens.el'. It uses `isar-long-id-stuff' inside the regexp which causes the whole word (identifier) to be subscripted. Is that wrong then?

The previous version (commented out) just used a single character but that didn't allow subscripted symbols. Current attempted fix: we now allow subscripted symbols but not subscripted control characters. If long id is wrong, please tell me the right regexp to use here!

I'm fine with that fix. It has the same effect as the old xemacs/xsymbol setup and seems to be compatible with the latex output.

[Norbert Schirmer]

Replying to da:

With respect to the issue with subsequent isubs, maybe introduce a proper ibsub..iesub region.

P.S., that's trivial to do inside isar-unicode-tokens.el, simply extend isar-control-regions in the obvious way (maybe: bisub, eisub for consistency!). But the Isabelle parser would need to be changed, wouldn't it?

Yes the lexer has to be adapted to accept the new control characters as letters This can be achieved by adapting src/Pure/General/syntax.ML accordingly. I am in favor of such an extension.

[David Aspinall]

P.S., that's trivial to do inside isar-unicode-tokens.el, simply extend isar-control-regions in the obvious way (maybe: bisub, eisub for consistency!). But the Isabelle parser would need to be changed, wouldn't it?

Yes the lexer has to be adapted to accept the new control characters as letters This can be achieved by adapting src/Pure/General/syntax.ML accordingly. I am in favor of such an extension.

OK, I have made the change inside PG now to add spanning super/subs, let's see if Makarius agrees to the lexer change. Unicode tokens supports many other typographic adjustments too, see etc/isar/TokensAcid.thy for examples.

[David Aspinall]

I'm fine with that fix. It has the same effect as the old xemacs/xsymbol setup and seems to be compatible with the latex output.

Thanks. I looked at the output of Display Draft and simplified it a bit more. See also #306.

[David Aspinall]

Closing this ticket now. Defaults seem reasonable and menu options work OK.

Remaining issues in other tickets: #311, #312, #313.

[David Aspinall]

See also #388

[David Aspinall]

See also #338