63 type perspective = (command_id -> bool) * command_id option; |
63 type perspective = (command_id -> bool) * command_id option; |
64 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
64 structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
65 |
65 |
66 type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo; |
66 type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo; |
67 (*eval/print process*) |
67 (*eval/print process*) |
68 val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []); |
68 val no_exec = |
|
69 Command.memo_value ((Toplevel.toplevel, {malformed = false}), []: Command.print list); |
69 |
70 |
70 abstype node = Node of |
71 abstype node = Node of |
71 {header: node_header, (*master directory, theory header, errors*) |
72 {header: node_header, (*master directory, theory header, errors*) |
72 perspective: perspective, (*visible commands, last visible command*) |
73 perspective: perspective, (*visible commands, last visible command*) |
73 entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*) |
74 entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*) |