diff options
author | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-03 18:22:09 +0000 |
---|---|---|
committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-03 18:22:09 +0000 |
commit | 66616778ed108dd21d1c9271f1d16e34048371e5 (patch) | |
tree | 4920e8d01ef44778c6b870e8feb7f9b1a5396f43 /ide/coq.mli | |
parent | a0299ca93ea3a0243e10caec1dc6e63e464178db (diff) |
Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1
This reverts commit 12537
This reverts commit 12199
This reverts commit 12198
This reverts commit 12172 (introduced the bug)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
-rw-r--r-- | ide/coq.mli | 37 |
1 files changed, 16 insertions, 21 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index a03528f81..3ded7b6bd 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -29,32 +29,22 @@ type printing_state = { val printing_state : printing_state -type reset_mark +type reset_mark = + | ResetToId of Names.identifier + | ResetToState of Libnames.object_name -type reset_info = { - state : reset_mark; - pending : identifier list; - pf_depth : int; - mutable segment : bool; -} - -val compute_reset_info : unit -> reset_info +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark -type backtrack = - | BacktrackToNextActiveMark - | BacktrackToMark of reset_mark - | NoBacktrack +type undo_info = identifier list -type undo_cmds = { - n : int; - a : int; - b : backtrack; - p : int; - l : (identifier list * int); -} +val undo_info : unit -> undo_info -val init_undo : unit -> undo_cmds +type reset_info = reset_status * undo_info * bool ref +val compute_reset_info : Vernacexpr.vernac_expr -> reset_info val reset_initial : unit -> unit val reset_to : reset_mark -> unit val reset_to_mod : identifier -> unit @@ -65,6 +55,11 @@ val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit val interp_and_replace : string -> (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string +val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool +val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool +val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool +val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool + (* type hyp = (identifier * constr option * constr) * string *) type hyp = env * evar_map * |