Re: [isabelle] Message output in Isabelle2014 and Isabelle2015
Yes â this might be OK.
> On 23 Jun 2015, at 13:42, Peter Lammich <lammich at in.tum.de> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and