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
diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala index b22613b..0d1e672 100644 --- a/src/Pure/General/symbol.scala +++ b/src/Pure/General/symbol.scala @@ -276,24 +276,24 @@ object Symbol private class Interpretation(symbols_spec: String) { /* read symbols */ - private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) private val Key = new Regex("""(?xs) (.+): """) private def read_decl(decl: String): (Symbol, Properties.T) = { def err() = error("Bad symbol declaration: " + decl) + def unescape_space(s : String) : String = s.replace("\\ ", " ") def read_props(props: List[String]): Properties.T = { props match { case Nil => Nil case _ :: Nil => err() - case Key(x) :: y :: rest => (x -> y) :: read_props(rest) + case Key(x) :: y :: rest => (x -> unescape_space(y)) :: read_props(rest) case _ => err() } } - decl.split("\\s+").toList match { + decl.split("(?<=[^\\\\])\\s+").toList match { case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props)) case _ => err()
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev