Email Gateway (Aug 22 2022 at 12:14): Email Gateway (Aug 22 2022 at 12:14):From: Peter Lammich <lammich@in.tum.de>
Hi,
after copying my personal etc/symbols file to the
~/.isabelle/Isabelle2016-RC1/etc/ folder, the command
"isabelle jedit" shows the splash-screen, and then freezes, never
displaying the editor, nor printing more messages to output. The
splash-screen displays "running startup scripts" when it freezes.
I attached the exceptions that are shown in the console, and my
symbols-file.
symbols
Email Gateway (Aug 22 2022 at 12:14):From: Lars Hupel <hupel@in.tum.de>
Hi Peter,
are you sure you only copied the symbols file and not the preferences
file, too? Judging by the error message, it looks like there is an
invalid "jedit_tooltip_delay" setting there.
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:14):From: Peter Lammich <lammich@in.tum.de>
I also copied preferences, but the crash behaviour can be triggered by
symbols. Removing symbols while keeping preferences and everything works fine
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:14):From: Lars Hupel <hupel@in.tum.de>
I also copied preferences, but the crash behaviour can be triggered by symbols.
Removing symbols while keeping preferences and everything works fine
You're right. I was under the impression that I also had a symbols file,
but didn't (I wonder where I put my custom symbols ...)
I tried reproducing the problem locally and apparently the offending
entry is
\<struct> code: 0x0022c4
(I found that by diffing Isabelle2015/etc/symbols and
Isabelle2016-RC1/etc/symbols.)
Removing that entry from your symbols file doesn't lead to a crash (on
my machine at least).
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:15):From: bnord <bnord01@gmail.com>
Maybe this was renamed to jedit_completion_delay ? etc/preferences
should be the file.
Best Benedikt
Email Gateway (Aug 22 2022 at 12:15):From: Peter Lammich <lammich@in.tum.de>
Thanks, that solved the problem for me. Still very unsatisfactory behaviour to
get a crash for an invalid symbols entry that was valid in the last version.
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:15):From: Makarius <makarius@sketis.net>
As a general principle, config files from $ISABELLE_HOME should not be
copied in full to $ISABELLE_HOME_USER, only the few lines that are
actually changed or added.
Your changes to etc/symbols are additional abbreviations. For
Isabelle2016 there is a new etc/abbrevs file that is briefly mentioned in
NEWS and has a small paragraph in the Isabelle/jEdit manual. The existing
$ISABELLE_HOME/etc/abbrevs can be taken as example for additions in
$ISABELLE_HOME_USER/etc/abbrevs.
Back to the mysterious error produced by Isabelle/jEdit as reaction to
present it old junk from Isabelle2015:
Command-line tools like "isabelle options -l" or variations on "isabelle
build" do produce this error (although without clear source position):
*** Duplicate mapping of "⋄" to "\<struct>" vs. "\<diamondop>"
The error is lost in the Isabelle plugin startup of jEdit, due to some
complications of object-oriented component initialization. Thus there is
basically an NPE, but my attempts to avoid NPEs in general caused a
meaningless error message instead. I've now refined that in the 3
changesets leading to
https://bitbucket.org/isabelle_project/isabelle-release/commits/027e6032977f
So in the next release candiate, there should be a lot of "Java vomit" and
spectacular dialog windows, containing variations of the above error
message.
You should nonetheless replace your old copy of etc/symbols by suitable
etc/abbrevs (without a copy of the official file).
Makarius
Last updated: Apr 26 2024 at 04:17 UTC