Email Gateway (Aug 19 2022 at 12:28): Email Gateway (Aug 19 2022 at 12:28):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, René Neumann wrote:
I tried theming my jEdit. It worked quite well (would probably take some
weeks of minor changes to get it in a sufficient state) but currently I
can't find a switch to change color of the general code inside quotes
(it remains black). Same applies for ML {* *}. Are there any?
There are many layers of formal markup, and many potential layers of
markup are suppressed for simplicity.
Above you can probably get along with quoted_color in "Plugin Options /
Isabelle / Rendering". It requires an alpha channel (transparency) to
work properly.
See also $ISABELLE_HOME/src/Tools/jEdit/src/rendering.scala for further
details. The markup trees that are interpreted here are somehow private
to the prover. They are mapped to certain public rendering parameters
defined in the "Rendering" section of Isabelle system options.
This configures the Isabelle/jEdit display engine, not the one of jEdit.
The latter is mainly defined by "Global Options / Syntax Highlighting" and
"Global Options / Text Area", but many of these colors have overrides in
Isabelle/jEdit. (I do my own text painting.)
(Bonus points if there is an extra category for the quotes, allowing to
remove them visually.)
In some sense, all these different quotes {...} "..." ''...'' and their
complicated rules for nesting are legacy. If one could assume that there
would be always some Prover IDE view on text, without TTY or Proof General
legacy, one could simplify that substantially -- both the syntax and
visual appearance of it. That is probably a bit speculative at this point,
where old XEmacs is still in use.
On the other hand, Isabelle2013-1 has already some visual devices that are
only visible in Isabelle/jEdit, like the "virtual bullets" for multiple
items in certain output.
Makarius
Email Gateway (Aug 19 2022 at 12:28):From: René Neumann <rene.neumann@in.tum.de>
Nope, this does not work. quoted_color is only used for the
_background_, not the foreground.
From looking at rendering.scala
…
Markup.STRING -> Color.BLACK,
Markup.ALTSTRING -> Color.BLACK,
Markup.VERBATIM -> Color.BLACK,
Markup.DELIMITER -> Color.BLACK,
…
they seem to be fixed to black :(
smime.p7s
Email Gateway (Aug 19 2022 at 12:54):From: René Neumann <rene.neumann@in.tum.de>
Hi,
I tried theming my jEdit. It worked quite well (would probably take some
weeks of minor changes to get it in a sufficient state) but currently I
can't find a switch to change color of the general code inside quotes
(it remains black). Same applies for ML {* *}. Are there any?
(Bonus points if there is an extra category for the quotes, allowing to
remove them visually.)
Last updated: Nov 21 2024 at 12:39 UTC