On Sun, 3 Jun 2012, Alexander Krauss wrote:
Technically, this situation represents a recoverable error (the
definition and the rest of the theory can be processed), but always
indicates a problem in the sources that should be fixed. It seems that
we do not currently have a corresponding severity level. Therefore
choosing between "ignored spam warning" and "break your leg error" is a
bit difficult.
Questions:
- Do we need a level for such messages/annotations? In IDE terms, a
little yellow triangle with an exclamation mark comes to my mind. I
wouldn't want to see this for most iother warnings, but here it might
make sense.
In principle the Prover IDE markup model supports arbitrary kinds of
messages and hilighting. Nonetheless one should reduce such things to the
bare minimum, such that tool authors still have a clear understanding what
is intended to be what message.
De-facto, the Isabelle/jEdit interpretation of plain-old warning and error
is slightly different than in Proof General:
* Warnings tend to be stronger, unlike PG where they often disappear.
* Errors tend to be weaker, because the (crude) recovery strategy will
skip over failed commands, and continue.
So yes, a duplicate constant definition is actually ignored.
Is it already possible for a package to emit a message/report that
carries position information, say to underline one of the clauses in a
specification processed by read_specification? This could also improve
the error reporting in other cases.
To affix messages to certain positions in the source one merely needs to
mention the position via Position.str_of somewhere in the message text.
This already works for approx. half of the prover messages.
For read_specification the position of the clauses in question are still
not passed through to the package. This will come some day, but needs at
least a tiny little bit of thinking, because clauses can conceptually
consist of several outer syntax term tokens (although that is not fully
implemented right now).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
