src/Pure/General/history.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23359 6e1786a6f636
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/history.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Histories of values, with undo and redo, and optional limit.
     6 *)
     7 
     8 signature HISTORY =
     9 sig
    10   type 'a T
    11   val init: int option -> 'a -> 'a T
    12   val is_initial: 'a T -> bool
    13   val current: 'a T -> 'a
    14   val previous: 'a T -> 'a option
    15   val clear: int -> 'a T -> 'a T
    16   val undo: 'a T -> 'a T
    17   val redo: 'a T -> 'a T
    18   val apply': 'a -> ('a -> 'a) -> 'a T -> 'a T
    19   val apply: ('a -> 'a) -> 'a T -> 'a T
    20   val map_current: ('a -> 'a) -> 'a T -> 'a T
    21 end;
    22 
    23 structure History: HISTORY =
    24 struct
    25 
    26 datatype 'a T =
    27   History of 'a * (int option * int * 'a list * 'a list);
    28 
    29 fun init lim x = History (x, (lim, 0, [], []));
    30 
    31 fun is_initial (History (_, (_, len, _, _))) = len = 0;
    32 
    33 fun current (History (x, _)) = x;
    34 
    35 fun previous (History (_, (_, _, x :: _, _))) = SOME x
    36   | previous _ = NONE;
    37 
    38 fun clear n (History (x, (lim, len, undo_list, redo_list))) =
    39   History (x, (lim, Int.max (0, len - n), Library.drop (n, undo_list), redo_list));
    40 
    41 fun undo (History (_, (_, _, [], _))) = error "No further undo information"
    42   | undo (History (x, (lim, len, u :: undo_list, redo_list))) =
    43       History (u, (lim, len - 1, undo_list, x :: redo_list));
    44 
    45 fun redo (History (_, (_, _, _, []))) = error "No further redo information"
    46   | redo (History (x, (lim, len, undo_list, r :: redo_list))) =
    47       History (r, (lim, len + 1, x :: undo_list, redo_list));
    48 
    49 fun push NONE _ x xs = x :: xs
    50   | push (SOME 0) _ _ _ = []
    51   | push (SOME n) len x xs = if len < n then x :: xs else Library.take (n, x :: xs);
    52 
    53 fun apply' x' f (History (x, (lim, len, undo_list, _))) =
    54   History (f x, (lim, len + 1, push lim len x' undo_list, []));
    55 
    56 fun apply f hist = apply' (current hist) f hist;
    57 
    58 fun map_current f (History (x, hist)) = History (f x, hist);
    59 
    60 end;