Opened 17 years ago
Last modified 11 years ago
#76 new enhancement
Add Prove-As-You-Type option
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
This is an idea for an updated version of the "electric terminator" option in PG Emacs.
If we parse behind the scenes, we can automatically send commands to the prover once they are completed. At first, this can be done just in case we are editing the command following the completed region.
- If the automatically sent command succeeds, the region can be moved forward and the output views updated.
- If the command fails, we would want to update the markers but probably not replace the output view (because the user may be referring to the current output to decide the next thing to write). An extract of the error will be available as the marker hover text, anyway.
- A possible user-annoyance is that the command succeeds but wasn't the one the user really wanted to use: so locking the region eagerly may cause frustration. Instead we might leave the new command region "unconfirmed", i.e. possible to commit given another UI action.
No specific support in the prover is needed for this, but an enhanced model of the proof script is needed, see #10.
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted