src/Pure/General/history.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23359 6e1786a6f636
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/history.ML
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     4
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
     5
Histories of values, with undo and redo, and optional limit.
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     6
*)
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     7
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     8
signature HISTORY =
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
     9
sig
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    10
  type 'a T
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    11
  val init: int option -> 'a -> 'a T
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    12
  val is_initial: 'a T -> bool
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    13
  val current: 'a T -> 'a
16496
8144814dc6a1 added previous;
wenzelm
parents: 15570
diff changeset
    14
  val previous: 'a T -> 'a option
7715
f90ec7937a7d clear: int arg;
wenzelm
parents: 6680
diff changeset
    15
  val clear: int -> 'a T -> 'a T
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    16
  val undo: 'a T -> 'a T
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    17
  val redo: 'a T -> 'a T
21175
98c0405f5493 replaced apply_copy by apply';
wenzelm
parents: 16496
diff changeset
    18
  val apply': 'a -> ('a -> 'a) -> 'a T -> 'a T
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    19
  val apply: ('a -> 'a) -> 'a T -> 'a T
23359
6e1786a6f636 renamed map to map_current;
wenzelm
parents: 21175
diff changeset
    20
  val map_current: ('a -> 'a) -> 'a T -> 'a T
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    21
end;
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    22
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    23
structure History: HISTORY =
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    24
struct
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    25
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    26
datatype 'a T =
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    27
  History of 'a * (int option * int * 'a list * 'a list);
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    28
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    29
fun init lim x = History (x, (lim, 0, [], []));
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    30
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    31
fun is_initial (History (_, (_, len, _, _))) = len = 0;
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    32
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    33
fun current (History (x, _)) = x;
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    34
16496
8144814dc6a1 added previous;
wenzelm
parents: 15570
diff changeset
    35
fun previous (History (_, (_, _, x :: _, _))) = SOME x
8144814dc6a1 added previous;
wenzelm
parents: 15570
diff changeset
    36
  | previous _ = NONE;
8144814dc6a1 added previous;
wenzelm
parents: 15570
diff changeset
    37
7715
f90ec7937a7d clear: int arg;
wenzelm
parents: 6680
diff changeset
    38
fun clear n (History (x, (lim, len, undo_list, redo_list))) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    39
  History (x, (lim, Int.max (0, len - n), Library.drop (n, undo_list), redo_list));
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    40
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    41
fun undo (History (_, (_, _, [], _))) = error "No further undo information"
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    42
  | undo (History (x, (lim, len, u :: undo_list, redo_list))) =
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    43
      History (u, (lim, len - 1, undo_list, x :: redo_list));
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    44
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    45
fun redo (History (_, (_, _, _, []))) = error "No further redo information"
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    46
  | redo (History (x, (lim, len, undo_list, r :: redo_list))) =
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    47
      History (r, (lim, len + 1, x :: undo_list, redo_list));
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    48
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    49
fun push NONE _ x xs = x :: xs
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    50
  | push (SOME 0) _ _ _ = []
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    51
  | push (SOME n) len x xs = if len < n then x :: xs else Library.take (n, x :: xs);
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    52
21175
98c0405f5493 replaced apply_copy by apply';
wenzelm
parents: 16496
diff changeset
    53
fun apply' x' f (History (x, (lim, len, undo_list, _))) =
98c0405f5493 replaced apply_copy by apply';
wenzelm
parents: 16496
diff changeset
    54
  History (f x, (lim, len + 1, push lim len x' undo_list, []));
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    55
21175
98c0405f5493 replaced apply_copy by apply';
wenzelm
parents: 16496
diff changeset
    56
fun apply f hist = apply' (current hist) f hist;
6680
7f97bb4f790d optional limit;
wenzelm
parents: 5039
diff changeset
    57
23359
6e1786a6f636 renamed map to map_current;
wenzelm
parents: 21175
diff changeset
    58
fun map_current f (History (x, hist)) = History (f x, hist);
5039
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    59
28c18f9e106e Histories of values, with undo and redo;
wenzelm
parents:
diff changeset
    60
end;