equal
deleted
inserted
replaced
15 val new_id: unit -> id |
15 val new_id: unit -> id |
16 val parse_id: string -> id |
16 val parse_id: string -> id |
17 val print_id: id -> string |
17 val print_id: id -> string |
18 type node_header = string * Thy_Header.header * string list |
18 type node_header = string * Thy_Header.header * string list |
19 datatype node_edit = |
19 datatype node_edit = |
20 Clear | |
20 Clear | (* FIXME unused !? *) |
21 Edits of (command_id option * command_id option) list | |
21 Edits of (command_id option * command_id option) list | |
22 Deps of node_header | |
22 Deps of node_header | |
23 Perspective of command_id list |
23 Perspective of command_id list |
24 type edit = string * node_edit |
24 type edit = string * node_edit |
25 type state |
25 type state |