[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts

[Rafal Kolanski]

When I wanted to customize my symbol font when switching to JEdit, I
realized that:

1. There is no separate symbol font setting, but JEdit does supply a
   nice cascading font substitution system (if glyph not found in
   main font, try next, then next, until optionally try every one
   in the system). It even lets you specify font sizes so their
   metrics match!

2. The Isabelle plugin doesn't use it. We do get a etc/symbols file,
   but it's a bit of an oddity. Unlike other parts of Isabelle source
   code which use parser combinators, this is thrown together with
   regular expressions.
   The lookup system then depends on compressing a maximum of two
   fonts plus other meta information (subscript, superscript, bold)
   for every JEdit chunk type (19 types) into a single Java byte...
   which is signed, so 127 tags is maximum. Is this done for speed?

   It's a bit of a shock to new users that after they specify their
   fonts the way they like, when JEdit loads everything looks great
   for a few seconds, and then most symbols turns to rectangles when
   the Isabelle plugin loads.

   I'd be willing to try address this issue, but I don't know if
   Makarius already has this in his pipeline already. I know it's
   pointless to try submit patches when work is already planned
   in accordance with a larger vision.

3. Trying to specify a font with a space in the name (e.g. Arial
   Unicode MS, Cambria Math) doesn't work, because the config lines
   in etc/symbols are split on \s+

Look, I realize I'm probably one of a handful of people on the planet
who specifies their own font preferences and color schemes, but I'd
appreciate the ability to do so. Call it being aesthetically challenged.

Attached is a workaround for Isabelle-2015, modifying
src/Pure/General/symbol.scala to allow escaping spaces when splitting
fields in etc/symbols.

I'm also sitting on two patches:

 - Work around the mouse select copy-paste issue for output/query/etc
   buffers.
   This is because the JEdit '%' register is updated for TextArea
   (see org/gjt/sp/jedit/textarea/MouseHandler.java ) when mouse is
   dragged, but for the Isabelle Pretty_Text_Area it isn't.

   Something a bit odd is going on here, because Rich_Text_Area inherits
   the correct behaviour implicitly, but not when it's included
   in Pretty_Text_Area. Maybe this needs more thinking.

 - Removes hardcoded colors in favor of looking up relevant JEdit
   properties. This is critical if you want a light-on-dark setup.
   Also in patches/extended_styles style[0] is hardcoded to black
   in org/gjt/sp/util/SyntaxUtilities.java. This should really look
   up the view.fgColor property in JEdit!

   Generally, defaulting to BLACK for foreground is inflexible, use:
	jEdit.getColorProperty("view.fgColor")
   same for 255,255,255 for a background, try use:
	jEdit.getColorProperty("view.bgColor")

Any interest in these? Does anyone else care?

Sincerely,

Rafal Kolanski
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabell2015_symbols_space_esc.patch
Type: text/x-patch
Size: 1206 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150825/307e670e/attachment.bin>