Re: [isabelle] Basic help with class and instantiation

On Thu, 16 Aug 2012, Yannick Duchêne (Hibou57) wrote:

Now to come back to an above comment I've made, which is “I often use it, but well, missed that” (talking about ctrl/command + mouse‑hovering over an item), may be an idea: show_types/consts/sorts, could still display something even when there is error to display. The Output pan did not show anything, as there was an error message instead, which replaced report messages. If both have been displayed together, may be I won't have missed it, as what's always displayed is less likely to be missed as I did.

This is just an area that is not fully covered by the Prover IDE markup yet. Just for Isabelle2012 I managed to get the inferred types into the annotations of the source text in the succesful case, which used to be an open problem for many years. The error case still needs to be refined in that respect, and then everyone will rightly take that for granted, so one needs to move further on to exhibit even more in the theory source.


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