Re: [isabelle] Message output in Isabelle2014 and Isabelle2015



On Di, 2015-06-23 at 10:19 +0200, Makarius wrote:
> (This is a relaunch of a thread that ended up containing mostly rubbish. 
> Here is another attempt to shed some light on the factual situation.)
> 
> 
> On Thu, 21 May 2015, Peter Lammich wrote:
> 
> > The output window shows the normal output (e.g. the current subgoals)
> > before the error output, (e.g. tactic failed).
> >
> > This is very inconvenient if the list of goals is longer, and you have
> > to scroll down every time to see the error message.
> >
> > In Isabelle2014, it was fine, and it showed
> >  errors, then normal output, then warnings.
> >
> > btw: I reported the same issue for some Isabelle2014-RCx, it got fixed
> > for 2014, and now we have it back again.
> 
> Can you explain precisely what you reported for Isabelle2014-RCx?  What 
> was the "issue" and what was the "fix".

As you pointed out, it was already discussed in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00115.html

in the release, the error messages then appeared before the subgoals,
or, more precisely, the subgoals did not appear explicitly at all, but
the error message contained a list of subgoals.

In Isabelle2015, the last goal state before the failing command seems to
get printed, too --- before the error message. This behaviour has a
positive and a negative effect on (my personal) workflow, which somewhat
coincides with your analysis:

  Positive: When typing commands, in particular those involving inner
syntax like <have "very-long-term">, I can see the current goal-state
all the time. In Isabelle2014 you saw "syntax error" or "type error"
most of the time, and had to go back with the cursor to see the
goal-state. I appreciate this behaviour, because, during typing such a
command, you are mostly interested in the previous goal state ... not in
the bogus information that you have a syntax error b/c typing is not
completed yet.

  Negative: As already reported before, if you have finished typing the
command, you are expecting that it works. If it does not, you are mostly
interested in the error message, and the proof state of the previous
command is of less importance.


As you point out, this behaviour was introduced in 2015. Note that the
overall problem was introduced with the processing model of PIDE, and
did not exist in Proof-General: There, by issuing a "goto this position"
- command, you told the IDE that you have finished typing, and now want
to focus on handling the errors.


> The deeper problem is cluttering of Output with too many different things, 
> and the lack of a dedicated panel just for proof state output. 
For those people with large screens, this may be a good solution. It
already worked nicely for PG, where I usually used the "3-pane" mode, or
had three windows: Text, Goal-state, Errors/Warnings. 

To make up for a nice layout, I would like to dock one panel to
right-top, and the other to right-bottom. Does jedit support such
docking positions, that go beyond left,right,top,bottom?


If you work on a small screen (laptop), you probably still want to have
a mode that consumes less space, and sensibly mixes the outputs.
However, I do not know how a PIDE-like asynchronous IDE can guess what
the user currently wants to see. Perhaps, you could try a heuristics on
the type of error, something like: 
Syntax-errors are displayed after the goal-state, failed method errors
before the goal-state.

Peter


















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