[isabelle] 2014-RC1 issues
Here is a list of issues that I encountered with RC1:
* 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
developing a theory. This leads to garbage accumulating in theory
files and probably only being discovered upon batch-build.
This feature may also cause surprises on bigger isar proofs, where it
is (in particuar as code-fold does not work) too easy to forget a qed.
* 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?
* 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.
* 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.
* 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and