diff options
| author | letouzey | 2011-09-05 16:47:26 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-05 16:47:26 +0000 |
| commit | c7d2cdb733f71f11ba9923d967d7b630958dfc83 (patch) | |
| tree | 949b5067ece992d6ae6db9e6049ced5801a1a62f /toplevel/ide_slave.mli | |
| 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 'toplevel/ide_slave.mli')
| -rw-r--r-- | toplevel/ide_slave.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli index 272616ae30..13dff280aa 100644 --- a/toplevel/ide_slave.mli +++ b/toplevel/ide_slave.mli @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Specialize loop of Coqtop for interaction with CoqIde *) - -val reinit : unit -> unit +(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp + function and a rewind function. This specialized loop is triggered + when the -ideslave option is passed to Coqtop. Currently CoqIDE is + the only one using this mode, but we try here to be as generic as + possible, so this may change in the future... *) val init_stdout : unit -> unit -val eval_call : 'a Ide_intf.call -> 'a Ide_intf.value - val loop : unit -> unit |