Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On Sat, 3 Oct 2015, Rafal Kolanski wrote: My priority at the moment is to see a release of jEdit, before we enter the critical release phase for Isabelle2016 -- presumably at the start of the Winter season here in the north. Once it is there, I will update the jedit_build component accordingly. Then we have a brief window of opportunity to add some small patches on top of the standard jEdit code base as part of the Isabelle distribution. Well, if you're already warning me that the window will be very small if and when it happens, then I would like to endeavor to make it count. If you find yourself with some spare cycles, perhaps you can do a Linus and take a look at my patch to Isabelle's font rendering to see if you like at all as a concept (there's a nice simplification to the rendering code in there in addition to the font substitution). If so, I can do extra work to make it more palatable to you / the Isabelle code base. If you don't like it, fair enough, and I'll just maintain a branch locally for my colleagues to use. I have lost track of the status of this thread, with its various side-threads on isabelle-users, isabelle-dev, and private mail. 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. Concerning the font substitution approach: Did you rethink my proposal to use the python interface of fontforge to assemble Isabelle font derivatives systematically? 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). 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
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
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On Tue, 15 Sep 2015, Rafal Kolanski wrote: The patched jedit code base will be updated again for the coming release of 5.3.0, which should appear *really*soon*now*. It will be the first jEdit release with proper 4K display support! Well, I hope they have time take a peek at some of the patches sitting in the queue before then... Right now I hope the jEdit guys will finally release the "Spring 2015" version before the winter comes on the northern hemisphere. jEdit 5.3.0 was planned to appear early June 2015. This summer I added various things on top of the repository version, expecting it to be post-release material, but they actually started picking it up after a few weeks and added most of it to the release branch. This caused further delays. My priority at the moment is to see a release of jEdit, before we enter the critical release phase for Isabelle2016 -- presumably at the start of the Winter season here in the north. Once it is there, I will update the jedit_build component accordingly. Then we have a brief window of opportunity to add some small patches on top of the standard jEdit code base as part of the Isabelle distribution. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 03/10/15 00:35, Makarius wrote: > On Tue, 15 Sep 2015, Rafal Kolanski wrote: > >>> The patched jedit code base will be updated again for the coming >>> release of 5.3.0, which should appear *really*soon*now*. It will be >>> the first jEdit release with proper 4K display support! >> >> Well, I hope they have time take a peek at some of the patches sitting >> in the queue before then... > > Right now I hope the jEdit guys will finally release the "Spring 2015" > version before the winter comes on the northern hemisphere. > > jEdit 5.3.0 was planned to appear early June 2015. This summer I added > various things on top of the repository version, expecting it to be > post-release material, but they actually started picking it up after a > few weeks and added most of it to the release branch. This caused > further delays. > > My priority at the moment is to see a release of jEdit, before we enter > the critical release phase for Isabelle2016 -- presumably at the start > of the Winter season here in the north. My patches to jEdit are pretty simple, but I understand if they only have a chance to be looked at after the release. > Once it is there, I will update the jedit_build component accordingly. > Then we have a brief window of opportunity to add some small patches on > top of the standard jEdit code base as part of the Isabelle distribution. Well, if you're already warning me that the window will be very small if and when it happens, then I would like to endeavor to make it count. Please consider that while you might not be able to take the patch now, you can use my time between now and then to make improvements. If you find yourself with some spare cycles, perhaps you can do a Linus and take a look at my patch to Isabelle's font rendering to see if you like at all as a concept (there's a nice simplification to the rendering code in there in addition to the font substitution). If so, I can do extra work to make it more palatable to you / the Isabelle code base. If you don't like it, fair enough, and I'll just maintain a branch locally for my colleagues to use. In particular, since my patch allows us to have multiple levels of sub/superscript (yes, only two, but still), perhaps you would like to see that in action before we put it in? Or some other way I can assist? Sincerely, Rafal Kolanski ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
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. * 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). * 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. 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. That is really old, one of the very first modules of Isabelle/Scala. It could have been updated to use Isabelle-style syntax, e.g. like session ROOT files. One reason why I did not do it: Isabelle symbol encoding is conceptually like a regular Java string encoding. Putting this at the very bottom of the JVM is possible, but extra library dependencies from Scala make it more difficult than necessary. So maybe one day I will actually re-implement that in Java 8, which is the most recent functional programming language on the market. 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. 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On Tue, 25 Aug 2015, Rafal Kolanski wrote:
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+
See the following changeset:
changeset: 61174:74eddfef841e
tag: tip
user:wenzelm
date:Mon Sep 14 17:39:29 2015 +0200
files: NEWS src/Pure/General/symbol.scala
description:
replacement character for spaces;
diff -r 5f3f203a38ad -r 74eddfef841e NEWS
--- a/NEWS Mon Sep 14 16:44:09 2015 +0200
+++ b/NEWS Mon Sep 14 17:39:29 2015 +0200
@@ -347,6 +347,11 @@
*** System ***
+* Property values in etc/symbols may contain spaces, if written with the
+replacement character "␣" (Unicode point 0x2324). For example:
+
+ \ code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono
+
* Command-line tool "isabelle jedit_client" allows to connect to already
running Isabelle/jEdit process. This achieves the effect of
single-instance applications seen on common GUI desktops.
diff -r 5f3f203a38ad -r 74eddfef841e src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala Mon Sep 14 16:44:09 2015 +0200
+++ b/src/Pure/General/symbol.scala Mon Sep 14 17:39:29 2015 +0200
@@ -289,7 +289,7 @@
props match {
case Nil => Nil
case _ :: Nil => err()
- case Key(x) :: y :: rest => (x -> y) :: read_props(rest)
+ case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) ::
read_props(rest)
case _ => err()
}
}
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 15/09/15 05:57, Makarius wrote:
> On Tue, 25 Aug 2015, Rafal Kolanski wrote:
>
>> - 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")
>
> I wonder where this strange light-on-dark trend is coming from, maybe
> from mobile devices? Many decades ago, monitor display quality was too
> poor for proper black-on-white text, which is why I consider this as
> luxory.
I can't speak for everyone, but my colleagues will attest to the fact
that my eyes are strange. I run my screens with 50% brightness,
light-on-dark and use custom stylesheets to recolor most of the internet
to be black-on-grey. You are right, and studies show this, that
white-on-black yields the highest contrast ratio and best readability.
Unfortunately, for people like me that effect lasts 15 minutes and then
I need to stop. With my current setup, even after 12 hours, my vision
doesn't get blurry at the end of the day. So it isn't purely aesthetic.
As for phones, they're going away from light-on-dark too (e.g. Android
Lollipop).
> Anyway, hardwired values are bad. I've changed most of them in
> 1d9c121cbe4d and 9791f631c20d.
Agreed, and thank you.
> The patched jedit code base will be updated again for the coming release
> of 5.3.0, which should appear *really*soon*now*. It will be the first
> jEdit release with proper 4K display support!
Well, I hope they have time take a peek at some of the patches sitting
in the queue before then...
Sincerely,
Rafal Kolanski
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
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
[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
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
