On Thu, 2 Dec 2010, Tobias Nipkow wrote:
The interface is a red herring. The discussion is on the concept at the
user level.
Here is again a current snapshot with everything built and bundled
http://www.lri.fr/~wenzel/Isar2010-Orsay/download.html
The new interaction model seriously changes the rules of the game. In the
past few month I've had many surprises how the system outputs information
to the user, which turned out as historical artifacts due to the
accidental Proof General message model.
Since the current issue is about user confusion, the user interface model
needs to be taken into account.
When the Prover IDE is starting to replace Proof General more seriously,
many messages, warnings, errors will have to be revised. I have already
started to think about the problem of implicit introduction of
polymorphism into the context in its many guises. Of course, I am
interested in good ideas from the standpoint of the new technology, i.e.
from anybody who has seriously tried Isabelle/jEdit already.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
