Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC2 beanshell errors

view this post on Zulip Email Gateway (Feb 11 2025 at 08:11):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,

I am sorry if this is not the right place to ask, but I encountered some
unexpected behaviors in Isabelle2025-RC2.
(If this is the right place to ask, I apologize for being late to report.)

I usually use Isabelle/jEdit with my own keybinding in MacOS (currently
Sonoma 14.5).
The customization is as follows.

1. Save the attached Emacs_Remap_keys.prop in $JEDIT_SETTINGS/keymaps,
and select "Emacs Remap" through
Isabelle > Settings > Global Options > jEdit > Shortcuts.

2. To activate the option key, add
Debug.ALT_KEY_PRESSED_DISABLED = false;
Debug.ALTERNATIVE_DISPATCHER = false;
in
/Applications/Isabelle2025-RC2.app/contrib/jedit-20250209/jedit5.7.0-patched/startup/startup.bsh.

However, I now get the two errors:

1. When I start Isabelle (through terminal), I get the error message in
the attached file Error_ALTERNATIVE_DISPATCHER.txt.
(Isabelle starts anyway, though.)

2. The Shortcut key such as Control+n does not work, and invokes the
error message in the attached file Error_ Accessibility.txt.

Since these errors are due to my own customization, there may be no problem
in Isabelle2025-RC2 itself.
However, I have not encountered such errors until Isabelle2024.
To be honest, I currently have no idea how to fix them.
I would be happy if you give me some workarounds.

Best regards,

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

Error_ALTERNATIVE_DISPATCHER.txt
Emacs_Remap_keys.props
Error_ Accessibility.txt

view this post on Zulip Email Gateway (Feb 11 2025 at 10:46):

From: Makarius <makarius@sketis.net>
On 11/02/2025 09:11, 伊藤洋介 wrote:

I am sorry if this is not the right place to ask, but I encountered some
unexpected behaviors in Isabelle2025-RC2.

I usually use Isabelle/jEdit with my own keybinding in MacOS (currently Sonoma
14.5).
The customization is as follows.

  1. Save the attached Emacs_Remap_keys.prop in $JEDIT_SETTINGS/keymaps, and
    select "Emacs Remap" through
    Isabelle > Settings > Global Options > jEdit > Shortcuts.
  2. To activate the option key, add
    Debug.ALT_KEY_PRESSED_DISABLED = false;
    Debug.ALTERNATIVE_DISPATCHER = false;
    in /Applications/Isabelle2025-RC2.app/contrib/jedit-20250209/jedit5.7.0-
    patched/startup/startup.bsh.

This is due to the update from jedit-5.6.0 to jedit-5.7.0, where the jEdit
guys have removed a few very old and deprecated things.

You can see the details like this:

diff -ru Isabelle2024/contrib/jedit-20240425/jedit5.6.0-patched
Isabelle2025-RC2/contrib/jedit-20250209/jedit5.7.0-patched

In particular, Debug.ALTERNATIVE_DISPATCHER and the keyboard dispatcher behind
it has been removed altogether. Many years ago, I was actually involved in
updating keyboard handling to make it work properly with Java 7.

Generally note that remapping keys in Isabelle/jEdit at a large scale is not
anything I would like to support.

Makarius

view this post on Zulip Email Gateway (Feb 11 2025 at 11:27):

From: Makarius <makarius@sketis.net>
On 11/02/2025 11:46, Makarius wrote:

In particular, Debug.ALTERNATIVE_DISPATCHER and the keyboard dispatcher behind
it has been removed altogether. Many years ago, I was actually involved in
updating keyboard handling to make it work properly with Java 7.

Looking once more, I think the alternative dispatcher has disappeared long
ago. So you may try without the obsolete flag Debug.ALTERNATIVE_DISPATCHER.

Makarius

view this post on Zulip Email Gateway (Feb 11 2025 at 11:45):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,

Thank you very much for the reply.
If remapping keys is not supported, I may follow your policy.

As for the second reply, I hope you could teach me one more thing.
I installed Isabelle2025-RC2 again from scratch, and I noticed that a
similar error occurred without any customization.
When I just select the existing keymap "Emacs" and push Command+n, an error
similar to "Error_ Accessibility.txt" occurs.
Is this also an intended behavior?

Best regards,

2025年2月11日(火) 20:27 Makarius <makarius@sketis.net>:

On 11/02/2025 11:46, Makarius wrote:

In particular, Debug.ALTERNATIVE_DISPATCHER and the keyboard dispatcher
behind
it has been removed altogether. Many years ago, I was actually involved
in
updating keyboard handling to make it work properly with Java 7.

Looking once more, I think the alternative dispatcher has disappeared long
ago. So you may try without the obsolete flag Debug.ALTERNATIVE_DISPATCHER.

Makarius

--
伊藤 洋介
080-5057-6931
glacier345@gmail.com

view this post on Zulip Email Gateway (Feb 11 2025 at 12:09):

From: Makarius <makarius@sketis.net>
On 11/02/2025 12:44, 伊藤洋介 wrote:

I installed Isabelle2025-RC2 again from scratch, and I noticed that a similar
error occurred without any customization.
When I just select the existing keymap "Emacs" and push Command+n, an error
similar to "Error_ Accessibility.txt" occurs.
Is this also an intended behavior?

Maybe that is a problem of jedit-5.7.0. You would have report that to the
jEdit project at Sourceforge, using an original jEdit installation from
https://www.jedit.org

For Isabelle/jEdit there are quite a lot of changes to the original: they are
formally recorded as Isabelle2025-RC2/contrib/jedit-20250209/jedit5.7.0.patch

Makarius

view this post on Zulip Email Gateway (Feb 12 2025 at 09:19):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,

Thank you for the additional information.
I confirmed that the original jEdit produces the same error.
On the other hand, I found a patch file which seems relevant to this issue.
https://sourceforge.net/p/jedit/patches/642/
Maybe this is what I am looking for?
(Just doing "patch" in terminal.app did not work, though.
I may have to take a closer look with jedit5.7.0.patch.)

Best regards,

2025年2月11日(火) 21:08 Makarius <makarius@sketis.net>:

On 11/02/2025 12:44, 伊藤洋介 wrote:

I installed Isabelle2025-RC2 again from scratch, and I noticed that a
similar
error occurred without any customization.
When I just select the existing keymap "Emacs" and push Command+n, an
error
similar to "Error_ Accessibility.txt" occurs.
Is this also an intended behavior?

Maybe that is a problem of jedit-5.7.0. You would have report that to the
jEdit project at Sourceforge, using an original jEdit installation from
https://www.jedit.org

For Isabelle/jEdit there are quite a lot of changes to the original: they
are
formally recorded as
Isabelle2025-RC2/contrib/jedit-20250209/jedit5.7.0.patch

Makarius

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

view this post on Zulip Email Gateway (Feb 12 2025 at 23:05):

From: Makarius <makarius@sketis.net>
On 12/02/2025 10:18, 伊藤洋介 wrote:

I confirmed that the original jEdit produces the same error.
On the other hand, I found a patch file which seems relevant to this issue.
https://sourceforge.net/p/jedit/patches/642

Maybe this is what I am looking for?

It looks good at first sight. I will take a closer look later ...

Makarius

view this post on Zulip Email Gateway (Feb 13 2025 at 09:46):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,

That is good to hear.
I really appreciate your help.

Best regards,

2025年2月13日(木) 8:05 Makarius <makarius@sketis.net>:

On 12/02/2025 10:18, 伊藤洋介 wrote:

I confirmed that the original jEdit produces the same error.
On the other hand, I found a patch file which seems relevant to this
issue.
https://sourceforge.net/p/jedit/patches/642

Maybe this is what I am looking for?

It looks good at first sight. I will take a closer look later ...

Makarius

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

view this post on Zulip Email Gateway (Feb 16 2025 at 19:56):

From: Makarius <makarius@sketis.net>
On 13/02/2025 00:05, Makarius wrote:

On 12/02/2025 10:18, 伊藤洋介 wrote:

I confirmed that the original jEdit produces the same error.
On the other hand, I found a patch file which seems relevant to this issue.
https://sourceforge.net/p/jedit/patches/642

Maybe this is what I am looking for?

It looks good at first sight. I will take a closer look later ...

It actually required more than one close look: the patch is not quite clear,
because it mixes up many "potentially useful changes". That could explain why
the jEdit guyes have ignored it so far.

I have reworked that patch for Isabelle/jEdit as follows:
https://isabelle-dev.sketis.net/rISABELLEa0d1d772ccab

Thus it will be in Isabelle2025-RC3, which is anticipated for 19-Feb-2025. In
the meantime you can try out a suitable snapshot from the isabelle-dev
repository: https://isatest.sketis.net/devel/release_snapshot

Anyway, using BeanShell for jEdit development is a rather bad idea: the
language is untyped and fragile, as we have seen here. Maybe the Emacs Macros
were originally done like that, because it approximates Emacs LISP pretty well.

If you are seriously interested in Emacs emulation in jEdit, I recommend to
make a proper plugin from that collection of BeanShell scripts, using Java ---
and then submit it to the jEdit project.

Makarius

view this post on Zulip Email Gateway (Feb 17 2025 at 12:29):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,

Thank you very much for the modification.
I have tested Isabelle_17-Feb-2025 and confirmed that the Emacs keybind
works correctly.
Honestly, I didn't realize that the original patch included extra
customization.
I am sorry for the inconvenience.
As you point out, I would reconsider remapping the keybind.

Best regards,

2025年2月17日(月) 4:56 Makarius <makarius@sketis.net>:

On 13/02/2025 00:05, Makarius wrote:

On 12/02/2025 10:18, 伊藤洋介 wrote:

I confirmed that the original jEdit produces the same error.
On the other hand, I found a patch file which seems relevant to this
issue.
https://sourceforge.net/p/jedit/patches/642

Maybe this is what I am looking for?

It looks good at first sight. I will take a closer look later ...

It actually required more than one close look: the patch is not quite
clear,
because it mixes up many "potentially useful changes". That could explain
why
the jEdit guyes have ignored it so far.

I have reworked that patch for Isabelle/jEdit as follows:
https://isabelle-dev.sketis.net/rISABELLEa0d1d772ccab

Thus it will be in Isabelle2025-RC3, which is anticipated for 19-Feb-2025.
In
the meantime you can try out a suitable snapshot from the isabelle-dev
repository: https://isatest.sketis.net/devel/release_snapshot

Anyway, using BeanShell for jEdit development is a rather bad idea: the
language is untyped and fragile, as we have seen here. Maybe the Emacs
Macros
were originally done like that, because it approximates Emacs LISP pretty
well.

If you are seriously interested in Emacs emulation in jEdit, I recommend
to
make a proper plugin from that collection of BeanShell scripts, using Java

and then submit it to the jEdit project.

Makarius

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

Last updated: Mar 09 2025 at 12:28 UTC