src/Pure/General/history.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 8806 a202293db3f6
child 14981 e73f8140af78
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@5039
     1
(*  Title:      Pure/General/history.ML
wenzelm@5039
     2
    ID:         $Id$
wenzelm@5039
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5039
     5
wenzelm@6680
     6
Histories of values, with undo and redo, and optional limit.
wenzelm@5039
     7
*)
wenzelm@5039
     8
wenzelm@5039
     9
signature HISTORY =
wenzelm@5039
    10
sig
wenzelm@5039
    11
  type 'a T
wenzelm@6680
    12
  val init: int option -> 'a -> 'a T
wenzelm@6680
    13
  val is_initial: 'a T -> bool
wenzelm@5039
    14
  val current: 'a T -> 'a
wenzelm@7715
    15
  val clear: int -> 'a T -> 'a T
wenzelm@5039
    16
  val undo: 'a T -> 'a T
wenzelm@5039
    17
  val redo: 'a T -> 'a T
wenzelm@6680
    18
  val apply_copy: ('a -> 'a) -> ('a -> 'a) -> 'a T -> 'a T
wenzelm@5039
    19
  val apply: ('a -> 'a) -> 'a T -> 'a T
wenzelm@6680
    20
  val map: ('a -> 'a) -> 'a T -> 'a T
wenzelm@5039
    21
end;
wenzelm@5039
    22
wenzelm@5039
    23
structure History: HISTORY =
wenzelm@5039
    24
struct
wenzelm@5039
    25
wenzelm@5039
    26
wenzelm@5039
    27
(* datatype history *)
wenzelm@5039
    28
wenzelm@5039
    29
datatype 'a T =
wenzelm@6680
    30
  History of 'a * (int option * int * 'a list * 'a list);
wenzelm@5039
    31
wenzelm@6680
    32
fun init lim x = History (x, (lim, 0, [], []));
wenzelm@6680
    33
wenzelm@6680
    34
fun is_initial (History (_, (_, len, _, _))) = len = 0;
wenzelm@5039
    35
wenzelm@6680
    36
fun current (History (x, _)) = x;
wenzelm@6680
    37
wenzelm@7715
    38
fun clear n (History (x, (lim, len, undo_list, redo_list))) =
wenzelm@7715
    39
  History (x, (lim, Int.max (0, len - n), drop (n, undo_list), redo_list));
wenzelm@5039
    40
wenzelm@6680
    41
fun undo (History (_, (_, _, [], _))) = error "No further undo information"
wenzelm@6680
    42
  | undo (History (x, (lim, len, u :: undo_list, redo_list))) =
wenzelm@6680
    43
      History (u, (lim, len - 1, undo_list, x :: redo_list));
wenzelm@5039
    44
wenzelm@6680
    45
fun redo (History (_, (_, _, _, []))) = error "No further redo information"
wenzelm@6680
    46
  | redo (History (x, (lim, len, undo_list, r :: redo_list))) =
wenzelm@6680
    47
      History (r, (lim, len + 1, x :: undo_list, redo_list));
wenzelm@6680
    48
wenzelm@6680
    49
fun push None _ x xs = x :: xs
wenzelm@6680
    50
  | push (Some 0) _ _ _ = []
wenzelm@6680
    51
  | push (Some n) len x xs = if len < n then x :: xs else take (n, x :: xs);
wenzelm@5039
    52
wenzelm@6680
    53
fun apply_copy cp f (History (x, (lim, len, undo_list, _))) =
wenzelm@6680
    54
  let val x' = cp x
wenzelm@6680
    55
  in History (f x, (lim, len + 1, push lim len x' undo_list, [])) end;
wenzelm@5039
    56
wenzelm@6680
    57
fun apply f = apply_copy I f;
wenzelm@6680
    58
wenzelm@6680
    59
fun map f (History (x, hist)) = History (f x, hist);
wenzelm@5039
    60
wenzelm@5039
    61
wenzelm@5039
    62
end;