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

1 files changed, 1 insertions, 1 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 685bfcac3..047a26587 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -47,7 +47,7 @@ val interrupter : (int -> unit) ref
 
 val interp :
   coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
-val rewind : coqtop -> int -> unit Ide_intf.value
+val rewind : coqtop -> int -> int Ide_intf.value
 val status : coqtop -> string Ide_intf.value
 val goals : coqtop -> Ide_intf.goals Ide_intf.value
 val inloadpath : coqtop -> string -> bool Ide_intf.value