Re: [isabelle] Remaining reasons for Proof General



On 12/11/13 09:17, René Neumann wrote:

- (obsolete: my WM fails to show jEdits dialogs. Just noticed that
there
is a patch available for it).

What is your WM?

i3

Never heard of that.  Consider it unsupported.

I never expected it to be supported. Supporting more than the very
mainstream software systems would be a nightmare, that I understand.
But please also allow me to ignore any 'only supported on'-disclaimers
(else I had a problem with many things).

I too use PG due to incompatibility between jEdit and my window manager
(Xmonad within Gnome Classic). Like René, I accept that this is a
Java-WM problem, not an Isabelle problem. I'm not really wed to any part
of my software stack so when PG truly stops working I'll make the call
to switch WMs or run jEdit in a VM.

There are many Linux guys who just don't want Java applications on
their particular fork.  The solution is to use one of the well-known
standard window managers.

That's not a solution, but a workaround (I'm using the WM I'm using
for good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and
is doing everything from scratch itself, I do not understand).

This is a very old argument of WM guys versus Java guys.  They hate each
other for that and accuse the other side of being wrong.

To be honest, the WM guys in question (ie i3 devs) never blamed anyone
in this particular case. It's just that such issues need their time to
be discovered and fixed.

For Isabelle/jEdit, I declare this issue as off-topic.  Users need to
use a well-known WM -- or join the OpenJdk project to solve the problem
themselves.

I've never thought Isabelle to be the one in charge here. That's why I,
after noticing this issue, opened a bug report on i3 [1] (a workaround
in the WM is easier than a fix in the JDK). It still counted as a
show-stopper for me regarding jEdit, though. (Which already got fixed, I
just included it in the email (marked 'obsolete'!) as I talked about
this with other users last Friday and wanted my list to be complete :)).

- René

[1] http://bugs.i3wm.org/report/ticket/1069


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.