Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2013-RC3 available for testing


view this post on Zulip Email Gateway (Aug 19 2022 at 10:01):

From: Christian Sternagel <c.sternagel@gmail.com>
I deliberately bought a laptop that does not have a keypad (not even
function-key emulation), since I never needed it, and then the other
keys have more space ;). (And this laptop is my main machine.)

What do you mean by "remap the non-keypad keys"? That I should use C-=
for font increase? (Which would be just fine.)

What I'm missing, though, is a way to go back to the default font-size
(like C-0 in firefox), I also did not find such a thing in the menus.
(When I change the font-size via C-foo C-bla and then close jEdit, will
it have the same degree of magnification when I start it again? If so,
C-0 would even be more relevant.)

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 10:01):

From: Makarius <makarius@sketis.net>
On Fri, 8 Feb 2013, Christian Sternagel wrote:

On 02/07/2013 11:36 PM, Makarius wrote:

On Thu, 7 Feb 2013, Christian Sternagel wrote:

On 02/07/2013 09:51 PM, Makarius wrote:

* Everybody: please check if you can scale the Isabelle/jEdit
font-size
up and down like in Firefox (C-PLUS/MINUS or C-ADD/SUBTRACT on the
keypad).
For me, Linux (Fedora 18) with us layout C-PLUS does not work (which
would actually be C-S-=), with ge layout both works fine (but then
again, there is no modifier S involved).

"Or" in my statement above usually means exclusive-or. On US keyboard,
you need the keypad or remap the non-keypad keys.
I deliberately bought a laptop that does not have a keypad (not even
function-key emulation), since I never needed it, and then the other keys
have more space ;). (And this laptop is my main machine.)

What do you mean by "remap the non-keypad keys"? That I should use C-= for
font increase? (Which would be just fine.)

Yes, you use the normal jEdit Options panel for keyboard shortcuts, and
press the respective keys.

So C-PLUS becomes C-= on UK/US/French keyboard on Windows and Linux, while
on Mac OS it becomes C-= C-= C-= (with this odd triplication due to Oracle
or Apple). Likewise, C-MINUS becomes C-6 on French keyboard.

To regain a little bit of sanity, the defaults for Isabelle2013-RC3 at
least look right, and often are right, but not always. I will put
this issue on the list of running gags, or rather bad jokes.

What I'm missing, though, is a way to go back to the default font-size
(like C-0 in firefox), I also did not find such a thing in the menus.
(When I change the font-size via C-foo C-bla and then close jEdit, will
it have the same degree of magnification when I start it again? If so,
C-0 would even be more relevant.)

jEdit does not support this model. So it is not really Firefox-style font
scaling, but just a shortcut to edit jEdit font properties via keystrokes.

Generally, I try not to avoid invading and assimilating too much of jEdit.
Going beyond that would mean much more engagement into the jEdit project
itself. After the Isabelle2013 release, I will again submit some patches
to some of their trackers, but it usually takes long to get attention
there.

Submitting problem reports to Oracle is yet another problem to be tackled
at some point. Anybody who feels like getting active is encouraged to do
so. The strange tribble C-= C-= C-= is a good starting point, it can be
reproduced with the KeyEventDemo from
http://docs.oracle.com/javase/tutorial/uiswing/events/keylistener.html in
JDK 7u13, for example.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Alfio Martini <alfio.martini@acm.org>
Hi,

In Windows, I just changed the shortcut (from Options Menu) C+ADD to
C+EQUALS and it works
fine again as in RC2 release. Therev are lots of possibilities there, it
seems.

Best!

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/8/2013 7:51 AM, Makarius wrote:

On Fri, 8 Feb 2013, Christian Sternagel wrote:

On 02/07/2013 11:36 PM, Makarius wrote:

On Thu, 7 Feb 2013, Christian Sternagel wrote:

On 02/07/2013 09:51 PM, Makarius wrote:

* Everybody: please check if you can scale the Isabelle/jEdit
font-size
up and down like in Firefox (C-PLUS/MINUS or C-ADD/SUBTRACT
on the
keypad).
What do you mean by "remap the non-keypad keys"? That I should use
C-= for font increase? (Which would be just fine.)
Yes, you use the normal jEdit Options panel for keyboard shortcuts,
and press the respective keys.

Neither works with the default .isabelle\Isabelle2013-RC3\jedit folder
for my Cygwin on Win7.

What I do different is I copy the unarchived Isabelle2013-RC3 folder to
where I want it, and then I start isabelle with a batch file with
environment variables set for where I want my home folder.

I also use a Windows 7 user account that doesn't have administrative
privileges.

I look in "imported_keys.props", and I see these:

isabelle.decrease-font-size.shortcut2=C+SUBTRACT
isabelle.increase-font-size.shortcut2=C+ADD
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.decrease-font-size.shortcut=C+MINUS

But, when I go to "Options/Global Options/Shortcuts" and filter on
"font", no shortcuts are registered there for increasing or decreasing
font sizes.

The other shortcuts I see in "imported_keys.props", I also see
"Options/Global Options/Shortcuts".

It's not a problem now, I manually added the font increase/decrease
shortcuts.

To regain a little bit of sanity, the defaults for Isabelle2013-RC3 at
least look right, and often are right, but not always. I will put
this issue on the list of running gags, or rather bad jokes.

There are jokes about fonts, and then there are Real and True
Conversations that I've heard, one of them being the following.

IsaUser1: Dude, who does Makarius think uses the size 18 font that comes
as the default for jEdit?

IsaUser2: Well, that would be Makarius himself. He uses a football
stadium size monitor, and at 50 meters, even a size 18 font is small, as
you can imagine.

IsaUser1: Dude, that is awesome! And I thought I liked to have a lot of
screen space when working with Isabelle.

IsaUser2: Oh no, it has nothing to do with Isabelle. It's for his
technical charts. He does day trading in his spare time.

IsaUser1: Bro, that's what I did, but not for very long, and I don't
think a stadium size monitor full of charts would have helped me out.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Alfio Martini <alfio.martini@acm.org>
(No email body)

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Makarius <makarius@sketis.net>
On Fri, 8 Feb 2013, Gottfried Barrow wrote:

IsaUser1: Dude, who does Makarius think uses the size 18 font that comes as
the default for jEdit?

It is an attempt to guess right in many first-encounter situations. 18px
also happens to be the size where the font that is used as basis for
IsabelleText (Bitstream Vera) renders with strong stems.

IsaUser2: Well, that would be Makarius himself. He uses a football stadium
size monitor, and at 50 meters, even a size 18 font is small, as you can
imagine.

In my office I do have a huge screen at 2560 pixel width, but that is in
fact not so much these days. The new "HD" displays (e.g. by Sony) or
"Retina" by Apple pose new challanges to applications to get something
visible on the screen. The top-end MacBook Pro fits 2560 pixels on a
rather small screen.

For Isabelle2013 I made several adjustments to accomodate the HD display,
either with Windows 8 or Linux. The "build" dialog that pops up at the
start was really tiny by default. Java/Swing defaults are still lagging
behind.

A remaining problem are menu sizes. I did already have the situation with
a digital projector from just 1 year ago at something like 1920 pixels,
rather than 1024 from the past. The main jEdit menus were very difficult
to see for the audience. The other extreme was an old one showing me
640x480, so I switched to 12px font and "Metal" look-and-feel to conserve
screen space, and it worked out.

We can all be glad that manual scaling of the IsabelleText font actually
works these days, unlike the bitmap fonts from some years ago.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Yes :-D (hope Makarius will enjoy his celebrity and the joke)

I personally change the font size to 14, check the “Use fractional font
metrics” option, and set anti‑aliasing to “standard”. These are my
personal defaults for Isabelle.

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
So now, to fewer people, it's not a mystery. However, as time passes,
there is the possibility that it will become, "canonical Isabelle humour".

Revisions and improvements are important in most areas of life, so to
raise the quality of this discussion, I submit a revision to the
previous Real and True conversation:

IsaJoke-2013-0208-0956

IsaUser1: [As before]

IsaUser2: [As before]

IsaUser1: [As before, or some meaningless variation using "dude", "bro",
"hommie" if you're a rapper, "mate" if you're Australian, "ole chap" if
you're British, or "kumpel", "fruend", "genosse", "matt", "maat",
"kamerad", or "gehilfe" if you're German.]

IsaUser2: Well, it's not just for Isabelle development. Makarius views
many, many technical charts at the same time. Makarius' day job is a day
trader. He only does Isabelle development in his spare time.

IsaUser1: [A user supplied sentence which overuses words like "dude" and
"awesome", and is meaningless, to keep the focus on the last sentence.]

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Makarius <makarius@sketis.net>
Anti‑aliasing to “standard” should already be the default -- it normally
works well across platforms with the exception of remote X11, but hardly
anybody does that now.

In contrast, "Fractional font metrics" turns out a trap on most
platforms that I have seen: it makes the font look blurry and bad. In the
early years of Isabelle/jEdit, I had spent a long time figuring out where
the problem was coming from, but did not manage to convince the jEdit guys
to be more explicit in its explanation.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:02):

From: Makarius <makarius@sketis.net>
I count this thread as part of carnival. Lets see if I manage to get
Isabelle2013 ready for Ash Wednesday next week (there are always 2-3 days
extra before final announcement).

Last orders can be made here as well:
https://bitbucket.org/isabelle_project/isabelle-release/issues

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:03):

From: Christian Sternagel <c.sternagel@gmail.com>
Well, I don't quite get the day trader joke, but the "German" words are hilarious.

Just for the record. I use the default font size on my laptop and with a not so big monitor, on neither of which the font seems too big. Moreover, as makarius pointed out earlier, for smaller font sizes the font is a bit "thin".

cheers

chris

Gottfried Barrow <gottfried.barrow@gmx.com> wrote:

view this post on Zulip Email Gateway (Aug 19 2022 at 10:03):

From: Arthur Peters <amp@singingwizard.org>
Isn't it possible to detect the DPI of the screen and set the font
accordingly? I thought all the modern text rendering libraries did this, so
you can set the font size in points and have it choose the correct pixel
size based on the size and resolution of the display. It seems that this
would solve the problem of the default being to big or small for some
people. And it might only require changing one thing to tell the system you
are using physical units instead of pixels.

Just a thought. Having people scale it themselves is not a big problem.

-Arthur

view this post on Zulip Email Gateway (Aug 19 2022 at 10:03):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/8/2013 9:05 PM, Christian Sternagel wrote:

Well, I don't quite get the day trader joke, but the "German" words are hilarious.

Day traders sit in front of multiple monitors looking at a bunch of
charts being updated in real time, so they would appreciate of a stadium
sized monitor.

http://lifehacker.com/5481921/the-day-traders-paradise

My basic setup is two jEdit views to edit the THY directly. A WinEdit
window to edit the ASCII source and run macros to convert and then build
to PDF. A Q-dir window with four folder views to view the file names of
my jEdit macros, which have the key sequence in their file name, and a
CubicExplorer window to get around and open files. That would only be to
edit files.

To view the math I'm trying to implement, and to try and learn Isar so I
can implement it, I need to read and compare a PDF or DJVU file to
what's in the editor window, or in another book.

I'm periodically tempted to upgrade to a 24 inch 1920x1080 for $130, so
I'll have a 1920x1080 and 1680x1050 instead of only a 1680x1050 and
1600x900. I could then use the 1600x900 on my laptop, instead of the
1024x768 that I'm using now.

Just for the record. I use the default font size on my laptop and with a not so big monitor, on neither of which the font seems too big. Moreover, as makarius pointed out earlier, for smaller font sizes the font is a bit "thin".
Decreasing even more my "chances of getting questions answered in the
future number", I pass on a Real and True conversation, where the "real
impact" of "Real and True" is much less than what it was before, if ever
it had any impact.

IsaUser1: Yo, homey, how does Christian get any work done using such a
huge font and small screen? There's only, like, 25 characters displayed
on his screen.

IsaUser2: Well, zuhausefreund, it is due to the size of his memory stack
value, which is calculated using his font size, 18, times the inverse of
the area of his screen size, which is relatively small. If you compare
his memory stack value with the memory stack value of someone like you,
who uses a small font and multiple monitors, then you will understand,
unless your small memory stack value is indicative of your total
cognition processing value.

Regards,
GB

cheers

chris

Gottfried Barrow<gottfried.barrow@gmx.com> wrote:

On 2/8/2013 9:32 AM, Makarius wrote:

On Fri, 8 Feb 2013, Gottfried Barrow wrote:

IsaUser1: Dude, who does Makarius think uses the size 18 font that
comes as the default for jEdit?
It is an attempt to guess right in many first-encounter situations.
18px also happens to be the size where the font that is used as basis
for IsabelleText (Bitstream Vera) renders with strong stems.
IsaUser2: Well, that would be Makarius himself. He uses a football
stadium size monitor, and at 50 meters, even a size 18 font is small,
as you can imagine.
In my office I do have a huge screen at 2560 pixel width, but that is
in fact not so much these days
So now, to fewer people, it's not a mystery. However, as time passes,
there is the possibility that it will become, "canonical Isabelle humour".

Revisions and improvements are important in most areas of life, so to
raise the quality of this discussion, I submit a revision to the
previous Real and True conversation:

IsaJoke-2013-0208-0956

IsaUser1: [As before]

IsaUser2: [As before]

IsaUser1: [As before, or some meaningless variation using "dude", "bro",
"hommie" if you're a rapper, "mate" if you're Australian, "ole chap" if
you're British, or "kumpel", "fruend", "genosse", "matt", "maat",
"kamerad", or "gehilfe" if you're German.]

IsaUser2: Well, it's not just for Isabelle development. Makarius views
many, many technical charts at the same time. Makarius' day job is a day
trader. He only does Isabelle development in his spare time.

IsaUser1: [A user supplied sentence which overuses words like "dude" and
"awesome", and is meaningless, to keep the focus on the last sentence.]

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 10:04):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
That info window popping up happened on me, but only after a day or so.

It might be related to a problem I haven't mentioned yet.

After the info window popped up this time, the output panel quit
printing any proof goal information. That was occasionally happening
with RC2, but, as I remember, the output panel stilled worked in the
view I wasn't working in, because the good view was what I would use to
make an A/B comparison to make sure it wasn't something simple I was
doing wrong.

This time, I had to close one view, open up a new view from the view
still open, and then open up a second view again.

Actually, I can't say without a doubt that the output panel quits
working when the info window pops up, because when I'm typing a lot, I
usually haven't been looking for output from the output panel.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 10:04):

From: Makarius <makarius@sketis.net>
The carnival is entering its hot and final phase ...

"Modern" things are just old things piled up over many decades. You can
ask for display DPI information on various platforms and various rendering
frameworks, but it often gives you just a constant value that happens to
be the most popular physical resolution of the time when these interfaces
were introduced. So it is 72 dpi for Mac OS (according to the first Mac)
and 96 dpi for X11/Linux (according to classic Sun workstations).

You can see how I tried it for my tiny build_dialog window here:

https://bitbucket.org/isabelle_project/isabelle-release/commits/4cd2d090be8f
https://bitbucket.org/isabelle_project/isabelle-release/commits/86389991636e

This was directly motivated by my brand-new Sony HD display. On Windows 8
I have specified a different DPI value explicitly, but MS lets certain old
Windows applications paint into a bitmap that is then scaled up. I think
that Apple plays other funny tricks with the even more dense Retina
displays to fool applications.

For Isabelle2013 it should all work suffiently well for now.

It is better to have fonts a bit too large by default than too tiny.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:06):

From: Makarius <makarius@sketis.net>
On Sat, 9 Feb 2013, Gottfried Barrow wrote:

After the info window popped up this time, the output panel quit
printing any proof goal information. That was occasionally happening
with RC2, but, as I remember, the output panel stilled worked in the
view I wasn't working in, because the good view was what I would use to
make an A/B comparison to make sure it wasn't something simple I was
doing wrong.

This time, I had to close one view, open up a new view from the view
still open, and then open up a second view again.

The observation is correct that every jEdit "view" has a separate
collection of "dockables" associated with it. The Output panel is one
such dockable. After some incident on the Java VM it could crash, so that
it no longer updates its window content. A fresh copy can be made via a
fresh view as sketched above, or just via "undock" and restart of the
dockable via the Plugins / Isabelle menu.

Actually, I can't say without a doubt that the output panel quits
working when the info window pops up, because when I'm typing a lot, I
usually haven't been looking for output from the output panel.

You could try to capture a Java VM exception trace next time, and show it
to me. I normally capture Java VM error output from the terminal, which
would mean Cygwin-Terminal for you and the command "isabelle jedit".

Alternatively, you can try the jEdit menu "Utilities / Troubleshooting /
Activity Log". That log should contain major failures of the running JVM
process -- jEdit has some command line options to moderate this a bit.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:29):

From: Makarius <makarius@sketis.net>
Dear all,

this is presumably the last release candidate for the Isabelle2013 that is
anticipated next week.

See https://bitbucket.org/isabelle_project/isabelle-release for the main
website where this is organized. There is also a link to an issue tracker on
the same Bitbucket site.

The main Isabelle2013-RC3 download page is
http://isabelle.in.tum.de/website-Isabelle2013-RC3

* Windows users: please check again that it all works. Former problems
with Cygwin file permissions should no longer happen.

* Mac OS X users: please check if you can quit Isabelle/jEdit properly.
There is now a handler for COMMAND-Q according to Apple, but it might
be in conflict with Oracle.

* Everybody: please check if you can scale the Isabelle/jEdit font-size
up and down like in Firefox (C-PLUS/MINUS or C-ADD/SUBTRACT on the
keypad).

Observations from testing release candidates may be discussed here on
isabelle-users, on the bitbucket tracker, or via private mail.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:30):

From: Christian Sternagel <c.sternagel@gmail.com>
For me, Linux (Fedora 18) with us layout C-PLUS does not work (which
would actually be C-S-=), with ge layout both works fine (but then
again, there is no modifier S involved).

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 10:30):

From: Makarius <makarius@sketis.net>
"Or" in my statement above usually means exclusive-or. On US keyboard,
you need the keypad or remap the non-keypad keys.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:30):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I'm running Isabelle on a laptop without a numpad, but still give it a
try: here, C‑MINUS do decreases the font size, but C‑PLUS do not increases
the font size (this one do nothing).

view this post on Zulip Email Gateway (Aug 19 2022 at 10:30):

From: Alfio Martini <alfio.martini@acm.org>
Hi,

C-PLUS/MINUS* work fine in jEdit/Isabelle RC2*. But in jEdit/Isabelle RC3
only C-Minus, as
mentioned below (Windows installation).

Best!


Last updated: Apr 23 2024 at 16:19 UTC