Opened 17 years ago
Last modified 11 years ago
#18 new enhancement
Add hover for prover output (on any blue space)
Reported by: | Owned by: | David Aspinall | |
---|---|---|---|
Priority: | minor | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
To support document-based editing without displaying intermittent output: can add a hover to display the latest prover output. It might be activated on whitespace area of processed region of latest command.
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted