On 16/11/15 07:14, Makarius wrote: > I have lost track of the status of this thread, with its various > side-threads on isabelle-users, isabelle-dev, and private mail.
All the patches I have sent out are still in effect w.r.t font rendering. > In the meantime the situation is as follows: > > * jEdit-5.3.0 has been released a few weeks ago, and we are using it since > Isabelle/d40f906bb13f. > > * I am still waiting for various plugin updates, notably Navigator. > > * There are still some fine points to be ironed out in main jEdit and some > plugins, i.e. bad GUI rendering on very high resolution displays. > > This means there will be a few small changes to the jedit_build > components, based on what the official jEdit project provides in the > coming weeks. This will not include any of my changes as no one has looked at my patches to jEdit since however many months ago I submitted them. > Concerning the font substitution approach: Did you rethink my proposal > to use the python interface of fontforge to assemble Isabelle font > derivatives systematically? So, concerning this situation, you are right and the correct way to go about font substitution is not to do it, or do it offline. Java's font substitution system is too poor to do what we want without massive effort. I am looking at the python+fontforge route, but making slow progress so far due to work commitments interrupting. However, that does not change the fact that your way of splitting chunks into little pieces every time you encounter an Isabelle symbol is inefficient. The patch I sent out in "Font substitution and handling in Isabelle/jEdit" on the 3rd of September contains a change, along with a small change to jEdit to expose some extra information. As I already stated multiple times in the past, that change needs to address font substitution because font substitution is a feature in jEdit. If someone enables it, then your rendering of chunks must still match up with jEdit's rendering of chunks, because you are overlaying one on the other. You currently split the chunks needlessly and use lots of IDs regardless of font substitution being enabled or not. With my change, font substitution still works, sure, but the important thing is it renders the entire jEdit chunk with a single call when font substitution is disabled. This simplifies memory layout and rendering code in the most common case which is the only case you want to support (i.e. everyone using IsabelleText font only). I really cannot say anything more unless you look at the patch I sent and see how the code changes. I don't know why that is not possible. > This would allow applications to use just one font. Thus the special > tricks of the jEdit text area won't be required. The result would also > work with plain Java Swing components, or in a completely different GUI > context (e.g. a web browser). Yes, and if you rip out font substitution from jEdit entirely, then my patch to rendering simplifies even more. > Note that the Isabelle-generated HTML pages already include the Isabelle > fonts since Isabelle/b3c665940d62 (and a few later changes). Other > fonts could be used as well, by modifications in the CSS. > > Thus we have a chance to get a uniform approach to Isabelle symbol > fonts, generated offline by some administrative python script. Sure, and generating these fonts offline will allow crazy people like me to have their own font which still includes all the glyphs necessary, satisfying both you and I. I will spend some evenings this week looking at scripting fontforge to generate IsabelleText. Could you please take a little while to look at my changes? I'm completely open to the idea of you not liking them and requesting further changes or rejecting them, but endless discussion without even looking really seems a waste of time. If no one looks at anything I do, then I can just keep a local fork going and keep quiet about the changes. Either way, I am not bringing this change up any more after this email, and consider it "rejected without consideration", along with the jEdit patches I submitted. For the record, all changes are still running along without any problems months later, and have been stress tested by working on the largest parts of the L4 verification project. Sincerely, Rafal Kolanski _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev