Re: [isabelle] Jedit: Spurious "Bad Theory" error



On Thu, 17 Oct 2013, Peter Lammich wrote:

This behaviour is really puzzling, I was already wondering what went wrong here, until somebody told me that it is normal for jedit to print some error messages on correct theories, that then magically disappear after some time.

The expectation seems to be immediate (synchronized) feedback by the tight real-eval-print loop from distant past. Isabelle/jEdit uses an asynchronous model that is hardly new, not even for IDE frameworks in general. When you manage huge amounts of information, it is more efficient (for the machine and the user) to give up the assumption of synchronous sequential command application.

To reduce confusion about the overall state of continuous checking the Theories panel is quite helpful -- it is docked by default and can be opened by a single click.

Moreover the overall text view is "greyed out" if the editor is still awaiting important feedback from the prover about already sumbitted edits.

More status overview and warning/error summaries (as seen in other IDEs) can be expected for the future, but old-style synchronous TTY interaction is not coming back.


	Makarius




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