optional limit;
is_initial;
apply_copy, map;

--- a/src/Pure/General/history.ML	Fri May 21 11:36:02 1999 +0200
+++ b/src/Pure/General/history.ML	Fri May 21 11:36:56 1999 +0200
@@ -2,18 +2,21 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Histories of values, with undo and redo.
+Histories of values, with undo and redo, and optional limit.
 *)
 
 signature HISTORY =
 sig
   type 'a T
-  val init: 'a -> '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 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
 end;
 
 structure History: HISTORY =
@@ -23,22 +26,35 @@
 (* datatype history *)
 
 datatype 'a T =
-  History of 'a * 'a list * 'a list;
+  History of 'a * (int option * int * 'a list * 'a list);
 
-fun init x = History (x, [], []);
+fun init lim x = History (x, (lim, 0, [], []));
+
+fun is_initial (History (_, (_, len, _, _))) = len = 0;
 
-fun current (History (x, _, _)) = x;
+fun current (History (x, _)) = x;
+
+fun clear (History (x, (lim, _, _, _))) = History (x, (lim, 0, [], []));
 
-fun clear (History (x, _, _)) = History (x, [], []);
+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));
 
-fun undo (History (_, [], _)) = error "No further undo information"
-  | undo (History (x, u :: undo_list, redo_list)) = History (u, undo_list, x :: redo_list);
+fun redo (History (_, (_, _, _, []))) = error "No further redo information"
+  | redo (History (x, (lim, len, undo_list, r :: redo_list))) =
+      History (r, (lim, len + 1, x :: undo_list, redo_list));
+
+fun push None _ x xs = x :: xs
+  | push (Some 0) _ _ _ = []
+  | push (Some n) len x xs = if len < n then x :: xs else take (n, x :: xs);
 
-fun redo (History (_, _, [])) = error "No further redo information"
-  | redo (History (x, undo_list, r :: redo_list)) = History (r, x :: undo_list, redo_list);
+fun apply_copy cp f (History (x, (lim, len, undo_list, _))) =
+  let val x' = cp x
+  in History (f x, (lim, len + 1, push lim len x' undo_list, [])) end;
 
-fun apply f (History (x, undo_list, _)) =
-  History (f x, x :: undo_list, []);
+fun apply f = apply_copy I f;
+
+fun map f (History (x, hist)) = History (f x, hist);
 
 
 end;