Opened 16 years ago

Closed 15 years ago

#222 closed enhancement (needmoreinfo)

Urgent messages override errors

Reported by: Makarius Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:
Cc:

Description

A feature of the message model which looks a bit odd to me: error messages can get lost if urgent messages follow.

Here is a synthetic example to get the idea:

ML {* Output.error_msg "failed"; priority "never mind" *}

Only the second message will be visible to the user.

In reality the error message stems from an actual failure of the command and the priority message is produced by some extra component that is not directly synchronized with the command execution.

Change History (2)

comment:1 Changed 16 years ago by David Aspinall

Milestone: PG-Emacs-3.7.1PG-Emacs-4.0
Status: newassigned

This "out of band" idea for the priority messages is a new interpretation for the message model, which never anticipated further output appearing after an error message.

We should re-examine the message model for PG 4.0.

comment:2 Changed 15 years ago by David Aspinall

Resolution: needmoreinfo
Status: assignedclosed

This needs some discussion. The current model in PG Emacs is to expect sequences roughly like this:

  JUNK
  ...
  URGENT 
  ...
  JUNK
  ...
  [GOALS]
  [RESPONSE] | [ERROR]

this is tuned to display URGENTs as soon as they appear, but ignore (possibly vast quantities of) JUNK. In particular, that includes GOALS, RESPONSE or ERROR that may appear before the URGENTs. At least in the old days, this sped up processing quite a lot as much output can be ignored. See doc of proof-shell-filter.

What would the ideal behaviour be for the current Isabelle? I suppose we could take the hit of parsing all the output (assuming provers are less noisy than before) and flag an ERROR if any appears. What output should be shown and in what order?

I guess the best way is to tie responses to commands that produced them as we did in PGIP, but that's a heavier change for Emacs.

Note: See TracTickets for help on using tickets.