--- a/src/Pure/General/history.ML Mon Jun 20 22:14:09 2005 +0200
+++ b/src/Pure/General/history.ML Mon Jun 20 22:14:10 2005 +0200
@@ -11,6 +11,7 @@
val init: int option -> 'a -> 'a T
val is_initial: 'a T -> bool
val current: 'a T -> 'a
+ val previous: 'a T -> 'a option
val clear: int -> 'a T -> 'a T
val undo: 'a T -> 'a T
val redo: 'a T -> 'a T
@@ -34,6 +35,9 @@
fun current (History (x, _)) = x;
+fun previous (History (_, (_, _, x :: _, _))) = SOME x
+ | previous _ = NONE;
+
fun clear n (History (x, (lim, len, undo_list, redo_list))) =
History (x, (lim, Int.max (0, len - n), Library.drop (n, undo_list), redo_list));