Re: [isabelle] Jedit: Spurious "Bad Theory" error
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] Jedit: Spurious "Bad Theory" error
- From: Makarius <makarius at sketis.net>
- Date: Tue, 5 Nov 2013 22:34:52 +0100 (CET)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <1381999643.4722.58.camel@lapbroy33>
- References: <1381999643.4722.58.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and