Email Gateway (Aug 19 2022 at 11:49): Email Gateway (Aug 19 2022 at 11:49):From: Tobias Nipkow <nipkow@in.tum.de>
I have tried to make the inner syntax in the theory window bold (in jedit).
Setting Utilities > Global Options > Text area > Text font > bold makes the
outer syntax bold but not the inner. This may well be intentional, but I may
just not have found the right menu item. Which one is it?
Thanks
Tobias
Email Gateway (Aug 19 2022 at 11:49):From: Makarius <makarius@sketis.net>
This might be actually a general jEdit question (potentially for the jEdit
mailing list at sourceforge), but in Isabelle/jEdit I also modify the way
fonts and jEdit "token markup" works, so one needs to look carefully what
happens where.
It seems that the jEdit text area font (the "view.font") can have its own
style (bold, italics etc), but that only applies to its use within plain
text, without any specific token markup (like quoted material or
comments). Only the font family is used to turn the view.font into token
styles. So the bold of the text area view.font is lost when it is turned
into the font style for quoted material.
One can see the effect when opening some .java file in plain jEdit, and
changes the text area font: only the non-special text is changed.
Actual token styles can be changed separately in the "Syntax Highlighting"
section of jEdit global options. Isabelle/jEdit has its own tokenizer for
theory files that uses the following jEdit tokens: KEYWORD2, LITERAL1,
LITERAL2, COMMENT1, COMMENT3.
For inner syntax it is LITERAL1 (for Isabelle "string" tokens) and
LITERAL2 (for Isabelle altstring tokens).
Alternatively, there is "Utilities / Quick settings / Edit syntax style of
token under caret". Then one does not need to know the token type in
advance. This menu item looks like a somewhat adhoc feature addition that
was added for exactly this situation :-)
Makarius
Last updated: Apr 25 2024 at 20:15 UTC