[isabelle] RC-3 puts method error after subgoals and warnings in output



In RC-3, I discovered the undesirable behaviour that errors are put
after the goal state in the output window. 

Example:

lemma "g1" "g2" "g3"
proof -
  have "False" by (simp add: list.simps)
 
  --> The error output appears after a list of the goals "g1" "g2" and
"g3" and after a long list of simplifier warnings.  


Thus, you have to scroll down to see the error output --- every time you
move the cursor in the main window from a different line to the
erroneous line. This is tedious when developing a proof, as you will go
up, change something, and then come back to the failing command multiple
times.

Moreover, the error is not visible as prominently as it used to be: 

When writing "have foo by method", expecting that it works, you look at
the output window ... and it looks the same, whether your method worked
or not. Formerly, you used to see a fat red error message there, right
at the top of the output window, which is now hidden.


If using separate outputs for error, warning, tracing, and goal is not
possible, and one must have a fixed order, I would vote for the
following order:
  Errors first, then the goal, then warnings, then tracing.

Of course, it would be even better to make the message types and the
order in which they appear in the output configurable!

--
  Peter





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