# HG changeset patch
# User wenzelm
# Date 1119298450 -7200
# Node ID 8144814dc6a1f4d94cfa8194c5ac5df503190802
# Parent  2e99aca906a776ac5a90936feb54f0c5ab612eda
added previous;

diff -r 2e99aca906a7 -r 8144814dc6a1 src/Pure/General/history.ML
--- 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));