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.

Change History (1)

comment:1 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0

Milestone PG-Eclipse-1.1.0 deleted

Note: See TracTickets for help on using tickets.