Re: [isabelle] 2014-RC1 issues

On Fri, 1 Aug 2014, Lars Noschinski wrote:

A type error in a ML_file disables ctrl+click and hovering for type annotations. Errors and warnings are still present. This behaviour does not occur in a ML block.

That is a consequence of the redirection of ML reports for external files, which reuses the asynchronous print infrastructure that I had presented at ITP2014 in order to swap-in and swap-out massive IDE markups on demand.

By making the print function non-strict wrt. the main eval phase, it can report static results even in the presence of failure: see d5b0fa6f1f7a, or the next release candidate.


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