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