Re: [isabelle] Isabelle2014-RC2 available for testing




Am 06.08.14 13:11, schrieb Makarius:
On Wed, 6 Aug 2014, bnord wrote:
When opening my Development in Isabelle/jEdit 2014-RC2 I got some (3-4) error markers that the theorem nat_add_commute was not found in some metis commands. I cleared them manually until all error markers were gone. Then when I restarted Isabelle/jEdit I got more error markers of the same kind, cleared them again manually until all were gone. But I still found 2 places were nat_add_commute was used using search afterwards which were not marked as errors.
According to NEWS there was a renaming of nat_add_commute ~> add.commute (and more like that).
Yes I figured that out, but my first go was just sledgehammer again which worked fine. Later I did a find/replace which edited two more occurrences.

Are you sure that the proof commands that still referred to this non-existing fact were actually applied successfully? I changed the error recovery recently, actually going back to some suggestions of yourself, but this change may now lead to some confusion.
No I wasn't sure just made the above observations. But I figured this one out now, just noticed that for long documents the bar on the right (whatever you call it) doesn't display markers for the whole document but only for some part. You have to scroll through the whole document after processing it to see whether there are any markers. This isn't what one is used to from other editors with such a feature.

Best
    Benedikt




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