Re: [isabelle] 2014-RC1 issues
On Wed, 30 Jul 2014, Peter Lammich wrote:
* If a lemma is not properly closed, ie. the done or qed is missing, the
next command only issues a warning and recovers the state. As warnings
are omnipresent in Isabelle, it is very hard to spot such places when
developing a theory. This leads to garbage accumulating in theory
files and probably only being discovered upon batch-build.
That is actually a contribution in Isabelle2014 to make error recovery a
bit more useful, without doing the real job of (sub)structural checking
What do you mean by "warnings are omnipresent in Isabelle"? The prover
IDE shows them more prominently than in the TTY past, but that could be
taken as motivation to remove the reasons for warnings. Not all such
spots are bad, but an avarage theory normally has only few warnings.
* In the output buffer, the standard Ctrl-Ins for "copy" does not work,
while it works in the main text area. Can these shortcuts be configured
separately? Or do I have to live with Ctrl-C?
I did not know about Ctrl-Ins yet. What you observe here is merely the
known and documented difference of the main jEdit text area with its
actions and shortscuts vs. regular Java Swing GUI components. The latter
only have basic Ctrl-C, and it actually works routinely, which is a big
step forwards to the historic perspective.
If Ctrl-C does *not* work somewhere, it is actually an issue that needs to
* Odd behaviour when focus lays in output buffer or any other panel:
Cursor movement and entering newlines still goes to the text area, but
other keyboard input goes to the panel (and may or may not be
interpreted there). The only indication for this is a slightly changed
color of the cursor in the main window.
This belongs to normal jEdit policies. In Isabelle/jEdit for the coming
release I added the faint cursor to emphasize that -- normally it would be
* No indentation feature. It is hard to keep track of big proofs and
indent them correctly, in particular as code-folding does not work
In PG, there was a nice auto-indentation feature that worked reliable
for (almost) all cases.
That is indeed a notable omission. In 1998, I added indentation to PG 2.x
quite early, and earned the name "The indentation Man" in the inner circle
of PG developers. In Isabelle/jEdit the lack of it has become a running
gag over the years: it needs to come one day, but so far I just wanted to
evade the wrath of users when the Prover IDE suddenly makes *standard*
indentation of Isar text by default.
* When developing proofs:
The output window displays the current position
by default ... if you are typing a new command, it usually displays
However, while typing your next method/isar step, you usually want to
see the current goal state, not a the completely useless information
In PG, the output was not updated before you explicitely processed
the command. Maybe, this can be simulated by turning auto-update off
and bind update to a convenient shortcut.
Nothing new about this observation. It belongs to general mismatch of
TTY/PG mechanics wrt. the document-oriented model. Note that you can also
use the Query panel to print proof states on demand and only on demand.
This archive was generated by a fusion of
Pipermail (Mailman edition) and