[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
  places when
  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
reliably.

  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
  "Syntax error". 
  However, while typing your next method/isar step, you usually want to
  see the current goal state, not a the completely useless information
  "syntax error".

  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.


--
  Peter






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