--- a/src/Pure/General/history.ML Tue Oct 05 15:26:10 1999 +0200
+++ b/src/Pure/General/history.ML Tue Oct 05 15:28:37 1999 +0200
@@ -11,7 +11,7 @@
val init: int option -> 'a -> 'a T
val is_initial: 'a T -> bool
val current: 'a T -> 'a
- val clear: 'a T -> 'a T
+ val clear: int -> 'a T -> 'a T
val undo: 'a T -> 'a T
val redo: 'a T -> 'a T
val apply_copy: ('a -> 'a) -> ('a -> 'a) -> 'a T -> 'a T
@@ -34,7 +34,8 @@
fun current (History (x, _)) = x;
-fun clear (History (x, (lim, _, _, _))) = History (x, (lim, 0, [], []));
+fun clear n (History (x, (lim, len, undo_list, redo_list))) =
+ History (x, (lim, Int.max (0, len - n), drop (n, undo_list), redo_list));
fun undo (History (_, (_, _, [], _))) = error "No further undo information"
| undo (History (x, (lim, len, u :: undo_list, redo_list))) =