equal
deleted
inserted
replaced
5 list of commands. |
5 list of commands. |
6 *) |
6 *) |
7 |
7 |
8 signature DOCUMENT = |
8 signature DOCUMENT = |
9 sig |
9 sig |
10 type state_id = int |
10 type id = int |
11 type command_id = int |
11 type exec_id = id |
12 type version_id = int |
12 type command_id = id |
13 val no_id: int |
13 type version_id = id |
14 val parse_id: string -> int |
14 val no_id: id |
15 val print_id: int -> string |
15 val parse_id: string -> id |
|
16 val print_id: id -> string |
16 type edit = string * ((command_id * command_id option) list) option |
17 type edit = string * ((command_id * command_id option) list) option |
17 end; |
18 end; |
18 |
19 |
19 structure Document: DOCUMENT = |
20 structure Document: DOCUMENT = |
20 struct |
21 struct |
21 |
22 |
22 (* unique identifiers *) |
23 (* unique identifiers *) |
23 |
24 |
24 type state_id = int; |
25 type id = int; |
25 type command_id = int; |
26 type exec_id = id; |
26 type version_id = int; |
27 type command_id = id; |
|
28 type version_id = id; |
27 |
29 |
28 val no_id = 0; |
30 val no_id = 0; |
29 |
31 |
30 fun parse_id s = |
32 fun parse_id s = |
31 (case Int.fromString s of |
33 (case Int.fromString s of |