diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:26 +0000 |
commit | c7d2cdb733f71f11ba9923d967d7b630958dfc83 (patch) | |
tree | 949b5067ece992d6ae6db9e6049ced5801a1a62f /test-suite/ide | |
parent | 0692216822e1fd9001f15178c5cb9dd91c9fbc74 (diff) |
Coqide: new backtracking code, based on the Backtrack command
This approach, inspired by ProofGeneral, is *much* simplier than earlier,
and should be more robust (I hope! feedback of testers is welcome).
Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
A stack on the coqtop side (in Ide_slave) convert this phrase count to
labels in the sense of Backtrack, and to abort + depth informations
concerning proofs.
We avoid re-entering finished proofs during Rewind by some extra backtracking
until before these proofs. The amount of extra backtracking is then answered
by coqtop to coqide. Now:
- for go_to_insert (the "goto" button), unlike PG, coqide replays
the extra backtracked zone.
- for undo_last_step (the "back" button), coqide now leaves the extra
backtracked zone undone, just like PG. This happens typically when
undoing a Qed, and this should be the only visible semantical change
of this patch.
Two points to check with Pierre C:
- such a coqtop-side stack mapping labels to opened proofs might be
interesting to PG, instead of passing lots of info via the prompt and
computing stuff in emacs.
- Unlike PG, we allow re-entering inside a module / section, while
PG retracts to the start of it. Coqide seems to work fine this way, to
check.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14455 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/ide')
0 files changed, 0 insertions, 0 deletions