src/Pure/General/history.ML

 sig
   type 'a T
   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
   val apply: ('a -> 'a) -> 'a T -> 'a T
   val map: ('a -> 'a) -> 'a T -> 'a T

 
 fun is_initial (History (_, (_, len, _, _))) = len = 0;
 
 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))) =
       History (u, (lim, len - 1, undo_list, x :: redo_list));