| author | wenzelm |
| Sat, 14 Aug 2010 22:45:23 +0200 | |
| changeset 38660 | 49f1f657adc2 |
| parent 38655 | e8197eea3cd0 |
| child 38677 | 9a7af64d71bb |
| permissions | -rw-r--r-- |
1 (* Title: Pure/PIDE/document.ML
2 Author: Makarius
4 Document as collection of named nodes, each consisting of an editable
5 list of commands.
6 *)
8 signature DOCUMENT =
9 sig
10 type id = int
11 type version_id = id
12 type command_id = id
13 type exec_id = id
14 val no_id: id
15 val parse_id: string -> id
16 val print_id: id -> string
17 type edit = string * ((command_id * command_id option) list) option
18 end;
20 structure Document: DOCUMENT =
21 struct
23 (* unique identifiers *)
25 type id = int;
26 type version_id = id;
27 type command_id = id;
28 type exec_id = id;
30 val no_id = 0;
32 val parse_id = Markup.parse_int;
33 val print_id = Markup.print_int;
36 (* edits *)
38 type edit =
39 string * (*node name*)
40 ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
42 end;