Re: [isabelle] 2014-RC1 issues



And you can't see the error in the Output panel either.

On 07/30/2014 01:42 PM, Lars Noschinski wrote:
On 30.07.2014 10:26, Peter Lammich wrote:
Here is a list of issues that I encountered with RC1:

And yet another issue: A method executing

    error ""

produces an error marker in the right sidebar. However, the associated
apply command does not get underlined in red and the error marker in the
left sidebar is missing.

Reproduce with:

theory Scratch imports Pure begin

lemma "PROP P"
   apply (tactic {* error "" *})
   oops

end






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