Re: [isabelle] sorry in innocent blue?

Somehow my "Bad Color" had been changed to be invisible.


On 13/05/2014 15:11, Makarius wrote:
> On Tue, 13 May 2014, Tobias Nipkow wrote:
>> I just spent more than half an hour trying to figure out where the problem
>> with my (long) poof was after I had discovered that the proposition was
>> definitely not true. Eventually I found a single sorry was left, attached to a
>> wrong claim. If sorry - which is definietly dangerous - had a dangerous
>> colour, I would have spotted it more quickly.
> In all official releases from 2013 there should be a "bad" markup for sorry,
> after it was processed by the prover.  That is neither an error nor a warning
> (so it does not show up in the buffer overview column nor the theories overview
> panel), but it has a thick red background and some tooltip to tell the reason
> for the relative "badness".
> If that special rendering was not to be seen, there might have been something
> wrong elsewhere.
>     Makarius

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