diff options
| author | vgross | 2009-11-19 12:48:32 +0000 |
|---|---|---|
| committer | vgross | 2009-11-19 12:48:32 +0000 |
| commit | 7a9708cd03e40bd9becb68d8e702be65d4992819 (patch) | |
| tree | a1e7b3eb9d90f6c20be8ae056694f6b5024ad715 /ide/coq.mli | |
| parent | 9a22ebe1d46b8f00980941ea0f54532595757f4e (diff) | |
Refactoring of coqide backtrack code, with the intent to put everything
into coqtop.
Also, some cleaning in ide/gtk_parsing.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index c2f96a1fe4..a03528f815 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -31,13 +31,30 @@ val printing_state : printing_state type reset_mark -type undo_info = identifier list * int +type reset_info = { + state : reset_mark; + pending : identifier list; + pf_depth : int; + mutable segment : bool; +} -val undo_info : unit -> undo_info +val compute_reset_info : unit -> reset_info -type reset_info = reset_mark * undo_info * bool ref +type backtrack = + | BacktrackToNextActiveMark + | BacktrackToMark of reset_mark + | NoBacktrack + +type undo_cmds = { + n : int; + a : int; + b : backtrack; + p : int; + l : (identifier list * int); +} + +val init_undo : unit -> undo_cmds -val compute_reset_info : unit -> reset_info val reset_initial : unit -> unit val reset_to : reset_mark -> unit val reset_to_mod : identifier -> unit |