[isabelle-dev] Redundant equations in function declarations

[Makarius]

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