# HG changeset patch
# User wenzelm
# Date 939130117 -7200
# Node ID f90ec7937a7d4bc9354114023e83fb768a6bab7c
# Parent  e6aa4fca983e1826db36e436ef1bd3c659a27a85
clear: int arg;

diff -r e6aa4fca983e -r f90ec7937a7d src/Pure/General/history.ML
--- 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))) =