added previous;
authorwenzelm
Mon Jun 20 22:14:10 2005 +0200 (2005-06-20)
changeset 164968144814dc6a1
parent 16495 2e99aca906a7
child 16497 474472ca4e4d
added previous;
src/Pure/General/history.ML
     1.1 --- a/src/Pure/General/history.ML	Mon Jun 20 22:14:09 2005 +0200
     1.2 +++ b/src/Pure/General/history.ML	Mon Jun 20 22:14:10 2005 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val init: int option -> 'a -> 'a T
     1.5    val is_initial: 'a T -> bool
     1.6    val current: 'a T -> 'a
     1.7 +  val previous: 'a T -> 'a option
     1.8    val clear: int -> 'a T -> 'a T
     1.9    val undo: 'a T -> 'a T
    1.10    val redo: 'a T -> 'a T
    1.11 @@ -34,6 +35,9 @@
    1.12  
    1.13  fun current (History (x, _)) = x;
    1.14  
    1.15 +fun previous (History (_, (_, _, x :: _, _))) = SOME x
    1.16 +  | previous _ = NONE;
    1.17 +
    1.18  fun clear n (History (x, (lim, len, undo_list, redo_list))) =
    1.19    History (x, (lim, Int.max (0, len - n), Library.drop (n, undo_list), redo_list));
    1.20