Re: [isabelle] RC1: etc/symbols file from 2015 crashes jedit tool on startup



On Thu, 21 Jan 2016, Peter Lammich wrote:

after copying my personal etc/symbols file to the ~/.isabelle/Isabelle2016-RC1/etc/ folder

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


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