Opened 10 years ago

Closed 8 years ago

#392 closed defect (wontfix)

Isabelle anti-quotation colouring obliterates symbol font setting

Reported by: Clemens Ballarin Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.2
Component: 2:pg-emacs Keywords:
Cc:

Description

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

Change History (3)

comment:1 Changed 10 years ago by 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.

comment:2 Changed 9 years ago by David Aspinall

Milestone: PG-Emacs-4.1PG-Emacs-4.2
Priority: majorminor

No great interest in this so bumping to 4.2

comment:3 Changed 8 years ago by David Aspinall

Resolution: wontfix
Status: newclosed

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

Note: See TracTickets for help on using tickets.