Opened 14 years ago
Closed 14 years ago
#303 closed defect (fixed)
underlining on error sucks
| Reported by: | Alexander Krauss | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
While others may report more fundamental problems, here is another usability issue:
Underlining the command that causes an error seems like a nice idea at first... But in reality it just sucks:
It does not give me any useful information, since I immediately see which command is broken anyway. To the contrary, the underlining makes it more difficult to spot the error, because the sources are much less readable. This becomes even worse if I happen to have the mouse over the thing. Then everything turns all red and I lose syntax highlighting...
I mentioned this over lunch and found out that some colleagues independently discovered the same workaround that I use: Move point to the command area, hit space, hit backspace to make the underlining disappear. Then keep on working.
Although it is meant to be a help, I think this is a big step backwards in usability. Is there a way to disable it? And it should be disabled by default.
Alex
Change History (2)
comment:1 Changed 14 years ago by
| Status: | new → accepted |
|---|
comment:2 Changed 14 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
This issue is fixed now, there is a new option `proof-sticky-errors' to control the underline. The default for underline has been changed to a red background colour. For more details, see the user manual.
I have reported the mouse faces hover problem as an Emacs bug, see here (in case that fragile looking URL breaks, the bug is number 4911).
Thanks for the robust feedback! Much appreciated.
I agree this stuff isn't so useful with PG's familiar mode of interaction. It was added to fit in with the "document centred" idea where you may turn off the ordinary background colouring and also the split screen display. Then realising where an error occurred may be less than obvious. See the updated user manual for details: I'd be very interested in feedback on that way of working.
The underlining is hard coded at the moment, but it has already been pointed out to me by a seasoned local user that underlining does not work well so should be something different. Also it would help to have a setting to turn off the sticky error effect, maybe.
Meanwhile, you can customize `proof-script-error-face' to prevent the red highlight.
It's annoying the mouse hover faces obliterate the underlying font-lock faces, rather than merge with them, I agree. Seems to be an Emacs hard-coded behaviour.