Re: [isabelle] Font substitution and handling in Isabelle/jEdit
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
index ac081b1..31db703 100644
@@ -405,6 +405,9 @@ class Plugin extends EBPlugin
PIDE.startup_failure = Some(exn)
PIDE.startup_notified = false
+ // new fonts loaded; references to them in config will now work
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.
On 03/09/15 10:32, Rafal Kolanski wrote:
> 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
> 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):
> 1. 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
> 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.
> 2. 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
> 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:
> - 0..n-1 : jEdit
> - n..2*n-1 : superscript
> - 2*n..3*n-1 : subscript
> - 3*n..4*n-1 : bold
> - 4*n..6*n-1 : user_font
> - 6*n : invisible (e.g. \<^sub> token itself)
> When jEdit sees these, it lays them out according to the extended style
> specified. We set these up to match the n jEdit styles, but tweaked in
> the desired way (size, font, style, elevation, etc).
> 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
> 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.
> Rafal Kolanski
This archive was generated by a fusion of
Pipermail (Mailman edition) and