Re: [isabelle] Message output in Isabelle2014 and Isabelle2015

Yes â this might be OK.

> On 23 Jun 2015, at 13:42, Peter Lammich <lammich at> wrote:
> One solution that does not involve too much implementation effort might
> be to not include the goal-state into the error message, and output this
> shorter error message *before* the goal-state. 
> While the user is typing, he would see a short error message that he
> could ignore, followed by the goal state. 
> When the user is inspecting the (error-)result of the command, he would
> see the error message first. Warnings should still be printed after the
> goal-state

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