Isabelle anti-quotation colouring obliterates symbol font setting

[Clemens Ballarin]

I can now get most symbols displayed by choosing "Apple Symbols" in the Tokens menu with the exception of symbols in antiquotations like @{term "\<Longrightarrow>"}. For these I need to commit to "Apple Symbols" for the whole buffer, from the Options > Appearance menue (which works with pre110131).

[David Aspinall]

This is the fault of the font lock keywords for anti-quotations, which works by obliterating the existing font lock settings when it adds the brown colouring, inadvertently changing the font back to the default buffer font. It wants to do that because the surrounding text has already been coloured by the comment syntax.

This is controlled by the "t", see line 412 of isar.el

   (cons isar-antiq-regexp '(0 'font-lock-variable-name-face t))))

As a workaround you can remove this line, but then you lose the colouring of anti-quotations.

A better fix would be to repair the way the font lock properties are merged in this case, which is possible but a bit delicate.

Makarius is responsible for the colouring markup, so I'll leave him to investigate that if he wants --- or anyone else from Isabelle team who can supply a patch, would be very welcome.

A clue is to look at some of the trickery in unicode-tokens.el which does similar merging, although it shouldn't be as hairy as that. The documentation of `font-lock-keywords' is the starting point.

[David Aspinall]

No great interest in this so bumping to 4.2

[David Aspinall]

Closing this as wontfix as seems unlikely anyone from Isabelle team will attempt to repair this.