On 15/09/15 01:15, Makarius wrote: > On Tue, 25 Aug 2015, Rafal Kolanski wrote: > >> 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! > >> The Isabelle plugin doesn't use it. > > This font-replacement mechanism is a relatively recent addition to jEdit > from a few years ago. The Isabelle/jEdit treatment of symbols, fonts, > text rendering preceeds that by 1 or 2 years. When the jEdit guys added > that feature, I noted it down on my TODO list immediately to revisit my > own approach. So far it did not happen for various reasons: > > * Font replacement only affects text area derivatives. For basic GUI > components it does not have any effect. We have some ugly tricks like > using HTML and IsabelleText font in some places, e.g. Sidekick entry > titles. Relying too much on font replacement would render that even > worse relatively to the text area.
I hope you have time to take a look at my suggestion (jEdit patch submitted upstream plus changes to Isabelle/jEdit rendering posted to the list on the 3rd of September). It addresses the issue of matching jEdit's substitution during rendering text area derivatives, and reduces chunk-splitting significantly. For basic components I do not presently have a solution. GTK2/3 just does a system-wide search to find missing glyphs, and Qt plugs into that, but the JDK doesn't. Maybe someday. > * The jEdit "Chunk" concept (text tokens to be rendered eventually) is a > bit odd. Looking myself too closely at it has a real danger of > spending a lot of time there to rework it. I still want to do it > someday, but it does not have top priority at the moment, in contrast > to things like proper GUI scaling (for "4K" displays on Windows and > Linux). I have not used jEdit long enough to decide how well the concept is executed, but the "chunk" setup seems not unusual for modern editors. If you were to do it again, which approach would you prefer? > * Java 6 on Mac OS X had its own super-smart font-replacement, and my > main work machine at that time was that platform. A bit too many > problems with such not-fully-working add-ons descreased the priority > further. Now we have standard Java 8 even on Mac OS X, and it > probably does not get in the way anymore, but I did not check it. On Linux (Ubuntu), I have not seen any form of font-replacement happen on the JDK for at least Java7/8. I do not recall it happening ever, so it may be a special OS X tweak. > [...] >> 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? > > Presumed "speed" is a lame reason for anything. I guess that Slava > Pestov simply did not know better when he made that many years ago. > There are a few more oddities at the bottom of text area and buffer > management, e.g. odd "split arrays" taken from Emacs. Without thise > mutable data non-sense -- with bytes, chars, arrays at the bottom -- > jEdit could be much faster and more scalable. This is a misunderstanding, the question was referring to why you did it that way, and after doing the work to implement the font substitution functionality, I understand now (and tried to document it as best I could in my long post on fonts/rendering). jEdit is strange to me in various ways. The type questions I get is "hey Raf, can you make parenthesis highlighting work in the output buffer?", or "why can't we pop over to the output/query window and select stuff with keyboard?". The answer is "not without modifying jEdit to add a virtual EditPane that allows sending keystrokes to a text area that isn't in an EditPane, otherwise jEdit will send it to the last active EditPane even though it's not focused" etc. >> 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 doubt that new users will specify fonts "the way they like". jEdit is > so flexible, that it can be configured in ways that Isabelle/jEdit no > longer works properly. We ship sane defaults, with a clear bias to > support one standard way that works well. Even just that is already > difficult to maintain. I know you are hesitant, but please take a look at the text area font substitution code I sent out if/when you have time. It does not affect existing features as shipped, except for a bit of improved memory efficiency due to less chunk splitting. It also frees up some IDs you can use for two levels of sub/superscript, which is a feature Gerwin has been asking me for (and bsub/bsup). The "unsurprising" part refers to the text area font substitution working when engaged, as compared to it ignoring you. Sure, there are one or two consequences, but they are the "you pressed the big red button didn't you" kind and not the "go away, we know better" kind. Thank you for adding the space escape mechanism to etc/symbols and for the constructive discussion! I wish I could just show you my changes working and explain how they work in person, but we are slightly too far for a coffee break meeting. Sincerely, Rafal Kolanski _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev