Email Gateway (Aug 22 2022 at 11:12): Email Gateway (Aug 22 2022 at 11:12):From: Rafal Kolanski <xs@xaph.net>
As you may know, the current font handling system in the Isabelle plugin
completely bypasses the one used in jEdit.
The symptoms of this are:
Global Options -> Text Area -> "Additional fonts with font
substitution" has no effect, confusing new users.
Can't use Your Favorite Font™ and have missing glyphs fall
back to the fonts you want.
Isabelle symbols can configure the font used, but there's a global
maximum of two user fonts (see user_font in token_markup.scala).
jEdit splits chunks at all Isabelle symbols
jEdit's font substitution system works really well. I wanted
Isabelle users to be able to benefit from it and enjoy tweaking fonts to
their heart's content, so I performed the necessary modifications to
make it work. The resulting code is simpler (though obviously Makarius
will tune naming to be more canonical) and I believe more
understandable.
I promised last week I'd deliver the change this week, and here it is.
I've also included some ad-hoc documentation on the situation and design
in the latter part of this email, hence its length. If you ever want to
tune the symbol/token/chunk system, this might be useful.
If you want to try it out, two patches are attached (use git apply):
jEdit: 0003-Allow-specification-of-sizes-for-fallback-fonts.patch
(see discussion at: https://sourceforge.net/p/jedit/patches/569/ )
This allows one to specify desired sizes for fallback fonts. The
reality is that font metrics between fonts don't agree. One font at
12 pt is the same size as another at 16 pt.
It also exposes queries on the font substitution system in Chunk.java
so that the plugin authors can use the information for their own
rendering.
This patch on its own does not affect existing jEdit/Isabelle users
and is safe to apply.
If you just want my version of jedit.jar, let me know.
Isabelle plugin: 0001-Redo-Isabelle-plugin-chunk-rendering.patch
(Isabelle 2015 version, but I can easily produce one that applies to
current development branch)
This removes the user_font setup in token_markup.scala and
modifies the paint_chunk_list code in rich_text_area.scala to match
the underlying chunk layout provided by jEdit even when font
substitution is enabled.
This depends on the jEdit patch (1).
The Outcome
You can now set up whatever font chain you want. For example mine is:
Lucida Console 16 -> Cambria Math 18 -> DejaVu Sans 16 -> IsabelleText
16 -> search all system fonts.
The setup is flexible enough that you can now use bizarre Unicode code
points (yes, even those above 0xFFFF) in your notation (output) if you
have the fonts to display it, e.g. I tested with:
U+1F0A4 PLAYING CARD FOUR OF SPADES
U+10147 GREEK ACROPHONIC ATTIC FIFTY THOUSAND
The chunk rendering code in rich_text_area.scala is simpler and should
be easier to understand.
By not using the user_font workaround, we free up 19*2 extended style
IDs that we can use for whatever we like. My suggestion: we can now do
two levels of super/subscript.
The "font" specification in etc/symbols now does nothing. Pick the
Unicode code point you want the symbol to display as and you're done.
The Details (only read if you are interested or Makarius)
jEdit's TextArea lays out chunks based on tokens it receives from the
relevant parser. Consecutive tokens with the same ID are grouped into
one chunk. One chunk has a single style (font, text color, background
color) plus a layout of GlyphVectors. If no font substitution was done,
the entire chunk is laid out as a single vector. Font substitution
splits vectors when the chunk is laid out, but the chunk is not split.
The Isabelle plugin provides a parser which lets jEdit parse and lay out
chunks. This results in inner syntax appearing as LITERAL1 (i.e. a
string). Once this process is done, all chunks are laid out, have
specified sizes and all font substitutions are done.
That's not the end of the story though. Once processed by Isabelle, we
acquire extra information. For example a part of that LITERAL1 is
actually a free variable, so should get a different text color! This
needs to be overlaid on the existing chunk somehow.
The way the Isabelle plugin performs the overlay of text colors is by
turning off the existing TextArea chunk renderer and doing the rendering
itself (see rich_text_area.scala). However, it isn't dumb and does not
lay out the underlying chunks again. This means that the rendering must
match up with the underlying chunk layout exactly in order to have the
glyphs and cursor appear in the right place within the chunk.
So if we want sub/superscript, we need to get jEdit to lay it out as
sub/superscript for us, or rendering our own ideas over it won't match
up!
There is a patch to jEdit (src/Tools/jEdit/patches/extended_styles)
which extends the n jEdit styles available (about 19) to 127 (max in
Java byte). That way we can do:
The user_font setup handles Isabelle symbols, but it's not very flexible
and it unnecessarily splits chunks (e.g. "sμn ⟶ mσσn" lays out as 9
chunks instead of one).
The renderer in Rich_Text_Area assumes one font per chunk, and user_font
only handles Isabelle symbols and not general code points present in the
text. The result is that with font substitution enabled in jEdit, using
code points not in your main font (yes, even IsabelleText has these)
will also result in glyph rendering misalignment.
As Isabelle plugin developers we cannot reuse the internal glyph
vectors stored in the chunk for rendering our text colors, because if
all code points are present in your main font, then "sμn ⟶ mσσn" will
not only be a single chunk, but also a single glyph vector. After it's
assembled, we can't get at which part means what.
So what do we do instead?
Create an AttributeString to contain all the rendering information for
the chunk. AttributeStrings are great. They store all style information
we need, but also font information.
For each Isabelle text color in the chunk, mark that range in the
AttributeString with that color, defaulting to chunk's default text
color and font. Mark where the cursor is as inverted-color.
Access the font lookup mechanism in Chunk.java (possible with the
patch). If jEdit didn't do font substitution, we don't either.
Otherwise: go through the AttributeString looking for code points the
chunk's font can't display. Ask Chunk if there's a substitute font to
use to display it. If there is, mark the range of the code point in the
AttributeString with that font.
Render resulting AttributeString. Watch as it lines up perfectly with
jEdit's layout regardless of what code points you dug out from the
depths of Unicode.
The end. It really is simpler, and I think a good change for Isabelle to
adopt.
Makarius: I know you probably won't like CustomChunk, or at the very
least its name. I just wanted to encapsulate the AttributeString
operations for simplicity and understandability. As always, if you're
not happy with something and want me to change/redo, let me know. I want
to make useful contributions.
Sincerely,
Rafal Kolanski
0003-Allow-specification-of-sizes-for-fallback-fonts.patch
0001-Redo-Isabelle-plugin-chunk-rendering.patch
Email Gateway (Aug 22 2022 at 11:26):From: Rafal Kolanski <xs@xaph.net>
There is a small update to this. Because some fonts (e.g. IsabelleText)
are dynamically inserted at Isabelle plugin load into the graphics
context after jEdit has loaded all properties ("settings"), jEdit
doesn't see them.
Since the Isabelle plugin makes changes to existing contexts that affect
the interpretation of jEdit properties, after some deliberation (and
about a week of testing) I suggest the following solution.
In src/Tools/jEdit/src/plugin.scala, at the end of the start() method,
we inform jEdit that it should look at its properties again:
diff --git a/src/Tools/jEdit/src/plugin.scala
b/src/Tools/jEdit/src/plugin.scala
index ac081b1..31db703 100644
--- a/src/Tools/jEdit/src/plugin.scala
+++ b/src/Tools/jEdit/src/plugin.scala
@@ -405,6 +405,9 @@ class Plugin extends EBPlugin
PIDE.startup_failure = Some(exn)
PIDE.startup_notified = false
}
+
Sorry for the noise. Getting this change right is important to me, and
feedback is a bit scarce. Now that Makarius potentially has time to look
at this, I want to offer as much assistance as I can.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 22 2022 at 11:33):From: Makarius <makarius@sketis.net>
I have recently made various reforms in the isabelle.Main vs. jedit.jar
initialization sequence, which is relevant for the coming winter release
of Isabelle2016.
If there are remaining problems, we should continue the discussion on the
isabelle-dev mailing list. The current point of reference is changeset
be3a5fee11e3.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC