Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dockable panels


view this post on Zulip Email Gateway (Aug 22 2022 at 12:09):

From: Lawrence Paulson <lp15@cam.ac.uk>
A trivial suggestion: The State panel should be docked to the bottom and not to the right.
Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 12:09):

From: Makarius <makarius@sketis.net>
Can you provide reasons for that suggestion?

Historically, I used to have main output at the bottom over many years,
but various side-conditions have changed. E.g. the 16x9 TV screen format
provides a lot of unused space on the right (for proper text lines of max.
80-100 chars). More and more Isabelle/jEdit users have switched to that
arrangement for Output in recent years (with slighly decreased font size).
I've merely picked up this trends myself, and find it quite convenient.

In Isabelle2016-RC1 the State panel takes that slot by default, and Output
at the bottom. Thus both panels can be open or closed indepedently.

In any case, rearrangement of dockables is trivial in jEdit, and
persistent, too.

Section 3.2 and 3.3 in
http://isabelle.in.tum.de/website-Isabelle2016-RC1/dist/Isabelle2016-RC1/doc/jedit.pdf
provide a few more words on that topic, also some pictures: figure 3.3 and
3.4. (That is my ancient Mac Book Pro without 16x9 display.)

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:09):

From: Lawrence Paulson <lp15@cam.ac.uk>
The obvious reason is that the output of the State panel needs a horizontal window. I imagine that most users will keep this window open all the time, and we can save them the trouble of having to re-dock it manually.

Everybody has their own style, and I almost never display the Output panel, since error messages can easily be viewed right in the main panel.

Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 12:10):

From: Makarius <makarius@sketis.net>
What is the format and resolution of your display?

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:10):

From: Lawrence Paulson <lp15@cam.ac.uk>
I am thinking of my laptop, which I use for most proofs. It is a 15 inch MacBook Pro. The screen is big enough for a substantial main window and a column on the right, perfect for panels such as Documentation, Sidekick, Theories and the ever-useful Timing.

With the latest models, the screen has very high resolution, but one can’t read microscopic fonts. Laptops are still widely used, I think.

Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 12:10):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Larry wrote:

With the latest models, the screen has very high resolution, but one can’t read microscopic fonts. Laptops are still widely used, I think.

Irrespective of this, even on a station, I find that it's easier to move my eyes up and down than left and right.

And when faced with a long goal, one surely wants to avoid wrapping as much as possible. This means taking the full screen width, not just half of it.

I know some people who e.g. edit their LaTeX document on the left half of their screen and look at the result on the right. I don't like doing that, and for this reason I keep both windows superimposed and continuously switch between them.

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 12:10):

From: Lars Hupel <hupel@in.tum.de>
I don't care so much about the defaults, but here's another data point
from my setup. I'm sympathetic for having state/output at the bottom.

(On a dual monitor setup, I undock the output panel and use it full
screen on the second monitor.)
Screenshot_20160119_122335.png

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: bnord <bnord01@gmail.com>
I second both points, also the vertical alignment allows you to scroll
the main buffer to a position where you have the relevant part of your
proof script only an inch away from the output, which is not possible in
the horizontal alignment where you always have to move your eyes over
the entire screen width.

Best
Benedikt

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Tobias Nipkow <nipkow@in.tum.de>
On 19/01/2016 12:24, bnord wrote:

Am 19.01.16 um 12:15 schrieb Jasmin Blanchette:

Larry wrote:

With the latest models, the screen has very high resolution, but one can’t
read microscopic fonts. Laptops are still widely used, I think.
Irrespective of this, even on a station, I find that it's easier to move my
eyes up and down than left and right.

And when faced with a long goal, one surely wants to avoid wrapping as much as
possible. This means taking the full screen width, not just half of it.
I second both points, also the vertical alignment allows you to scroll the main
buffer to a position where you have the relevant part of your proof script only
an inch away from the output, which is not possible in the horizontal alignment
where you always have to move your eyes over the entire screen width.

This ability to align text in both buffers and compare it is what I find most
useful.

Tobias

Best
Benedikt

smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Makarius <makarius@sketis.net>
We are back to field one of the game.

The most widely used Laptops (for more than 3 years) have a 16x9 TV
screen. The lines for that are far too wide for text, although people
sometimes mistake the TV format to produce unreadable 250 characters per
line.

When used properly, a 16x9 display consists of two full-width text
displays side by side. This explains the position of the proof state panel
(and other important "dynamic" panels like "Theories" or "Timing").

Nobody is forced to use that default. It is just for people who don't
look closely by themselves.

Changing these things is rather trivial, and actually explained in the
Isabelle/jEdit manual (with an explicit reference to the jEdit
documentation).

Now we are back to the more fundamental question if anybody reads
documentation at all. There should probably be also a video presentation.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: bnord <bnord01@gmail.com>
Dear Makarius,

the documentation is really well done and I relay appreciate the amount
of work you put into it!

However the honest answer is probably that only a very small percentage
will "look into" the documentation and an even smaller percentage of
those people will actually "read it"t. This doesn't mean that the
documentation is bad or unnecessary, but we've all been educated to
expect software (especially GUIs) to work intuitively and be able to get
it to do what we want by try and error and only refer to the
documentation if we really care and can't get it done otherwise, which,
for most other software, leads to disappointment, because, if the
developer didn't put effort into making things intuitive, he often also
didn't put effort into documenting them.

I personally dislike video presentations, because it's hard to figure
out whether they cover what you're interested in, without actually
watching them and then they're often either too slow or too fast.

Best
Benedikt

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Makarius <makarius@sketis.net>
I know what you mean.

I've actually read one (!) textbook about UI design: "About Face 3". It
tells many such stories.

My own experience as someone hopping between the many UI frameworks of
Linux, Windows, Mac OS X: Intuitive is what you know already. What you
don't know is unintuitive.

Confronted with funny GUI elements like the dockables in jEdit, I would
first try a single left click, a single right click, a double click, and
watch carefully what happens. On Linux and Windows this quickly exposes
the dockable control menu (right click) to move it into a different
corner or let it float. So I guess it requires about 10 seconds to learn
that trick.

On Mac OS X: What is a right click? (My own OS X preferences enable all 3
mouse buttons, but that is hardly a common default).

Here we see a bias of the jEdit developers (and Java AWT/Swing) to
"standard" GUI behaviour of Windows (and imitations of the same in Linux).

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Makarius wrote:

Nobody is forced to use that default. It is just for people who don't look closely by themselves.

Changing these things is rather trivial, and actually explained in the Isabelle/jEdit manual (with an explicit reference to the jEdit documentation).

Now we are back to the more fundamental question if anybody reads documentation at all.

You asked a few emails ago:

Can you provide reasons for that suggestion [changing the default position]?

And now we give you reasons for changing the default (in Isabelle, not on our machines), and you tell us we should read the documentation. There is a disconnect between what you asked for, what you got from us, and how you reacted to it.

I am not adamant about how Isabelle's default should be -- nobody seems to be on this list, as long as there is a way to override it.

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Makarius <makarius@sketis.net>
I am not sure what I've actually got.

Is there a problem for seasoned OS X users to guess how jEdit dockables
are moved around? This is a plain question, not a rhetoric one. (I am not
a seasoned OS X user, although I am occasionally running it for 10 years.)

The point of the default arrangement is to make it work out-of-the box for
most users, beginners and experts alike. It is the result of the past 3
years looking closely what beginners and experts have, or could have.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:11):

From: Lawrence Paulson <lp15@cam.ac.uk>
I would say it’s not about how to move things around, but how the defaults should be, especially since State is a new panel. As others have noted, putting it at the bottom has a number of advantages, and I can’t see any advantages of putting it at the right. The out-of-the-box defaults are pretty good, I think they could be even better.

Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: Makarius <makarius@sketis.net>
In this proposal, what is the canonical place for the Output dockable?

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t mind, as I almost never use it. I use the red underlines to examine error messages. But personally I have it on the bottom as well.
Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: bnord <bnord01@gmail.com>
Even though I highly prefer having the state output at the bottom due to
the previously stated reasons I would maybe consider not having it the
default for the following reason:
For beginners visibility is more important than comfort.

In the current (2015) default setting the output panel is conflicting
with the Sledgehammer panel. I have observed students (which in my
experience sadly rely a lot on sledgehammer) become oblivious of the
proof state and try to create proofs by just typing in stuff and running
sledgehammer. They get completely lost when you tell them to look at
their proof state to and try to understand why things don't work.

If the horizontal alignment helps to have all panels visible at all
times I'm in favour of having this the default as non-beginners can
still change this to their desire.
If the same can be achieved with the vertical alignment I'm in favour of
this because it's more comfortable and puts the most important panel
(IMHO) at the most prominent place.

Best
Benedikt

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>

Is there a problem for seasoned OS X users to guess how jEdit dockables are moved around? This is a plain question, not a rhetoric one. (I am not a seasoned OS X user, although I am occasionally running it for 10 years.)

I've been using OS X exclusively since 2008 and I don't know how to move the State panel to the bottom. (I haven't read the docs either; I've enabled the "Proof state" feature to get the old school behavior.) I don't see any grip on the panel which I could use to move it around, so I don't know where to click (seriously). I should indicate that I'm using the Macish style whereby the jEdit menu bar is merged with the Mac menu bar.

I don't use that many applications, but those I use (e.g., Preview, Skim, Apple Mail, iTunes, Safari, Keynotes) have no dockable panels. Apple probably don't like them.

The point of the default arrangement is to make it work out-of-the box for most users, beginners and experts alike. It is the result of the past 3 years looking closely what beginners and experts have, or could have.

I can only speak for myself, but it does feel suboptimal to put contents that has a large horizontal component and (usually) a small vertical component in an area that has, in the best case, a squarish shape, and in the worst case much more vertical space than horizontal space.

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: bnord <bnord01@gmail.com>
It's hidden under the not very descriptive triangle-down symbol, maybe
something like [1] would be more intuitive.

[1]
http://www.iconarchive.com/show/farm-fresh-icons-by-fatcow/layout-content-icon.html

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: bnord <bnord01@gmail.com>
I tried leave the old habits of the 2 buffer approach behind me and
adopt a new layout. I tried to create the following layout but failed to
place several panels always visibly docked at the right, is this
possible? I don't like having to switch between tabs.

| sidekick
main |---------------
| sledgehammer
-------|---------------
state | output

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: Makarius <makarius@sketis.net>
No, that is actually an FAQ on this mailing list. The default Dockable
Window Manager only allows one active dockbale per docking area.

Internally, there is a more generic "service" interface, to plug-in
different dockable window managers; this was done once with the MyDoggy
plugin. Both MyDoggyPlugin and the original MyDoggy project are inactive,
though.

There should be more modern and active docking frameworks on the free
Java/Swing market, but it requires some time to look around, and then more
time to make it work as a usable jEdit plugin.

Such a project could be done by any Java Swing enthusiast, and submitted
to the jEdit project at Sourceforge. It would be a great step forwards.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: bnord <bnord01@gmail.com>
Thanks that's unfortunate. While the environment allows for only 3
active panels (I don't think one would want to put one on the top and
left also) one should probably avoid separating things like
output/state/sledgehammer etc. to different panels. I might look into
finding other docking frameworks but I doubt that I'll find the time to
integrate them.

Best
Benedikt

view this post on Zulip Email Gateway (Aug 22 2022 at 12:12):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
If I put two panels side-by-side on my laptop, my aging eyes are too
feeble to be able read the contents. So mine is another vote for a
horizontal Output panel.

It would be very helpful if an undocked Output panel could be made so
that it is not "always on top". Is this possible (on Ubuntu/Unity)?
I didn't see how to do it, but if I could do it I would arrange the
windows to be overlapping and I would raise and lower the one I want
to see.

- Gene Stark

view this post on Zulip Email Gateway (Aug 22 2022 at 12:13):

From: Makarius <makarius@sketis.net>
There is a hardwired policy in Java/AWT, which is implicitly exposed by
the classes JFrame vs. JDialog. An application has to make a choice which
one to use. I've made that choice for JDialog some years ago, when it
became apparent that JFrame can lead to situations where windows become
inaccessible on certain platforms with certain window managers, especially
with full-screen mode.

So with a choice between slightly inconvenient window stacking versus
inoperable windows, I've taken the slight inconvenience.

To really solve that problem, one probably needs to avoid AWT, and go for
JavaFX. That might actually work, because FX allows to integrate
AWT/Swing panels within its GUI containers, but I have no experience with
that.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:25):

From: Simon Wimmer <wimmersimon@gmail.com>
Another way is to use Control+Click on the text selector text "State" of
the state panel, keeping the mouse button pressed, and selecting one of the
"Dock at x" options (the same options are in the triangle menu). However,
this is not really more intuitive, I guess.


Last updated: Nov 21 2024 at 12:39 UTC