equal
deleted
inserted
replaced
14 val no_id: id |
14 val no_id: id |
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 edit = string * ((command_id option * command_id option) list) option |
18 type edit = string * ((command_id option * command_id option) list) option |
|
19 type header = string * (string * string list * string list) |
19 type state |
20 type state |
20 val init_state: state |
21 val init_state: state |
21 val get_theory: state -> version_id -> Position.T -> string -> theory |
22 val get_theory: state -> version_id -> Position.T -> string -> theory |
22 val cancel_execution: state -> unit -> unit |
23 val cancel_execution: state -> unit -> unit |
23 val define_command: command_id -> string -> state -> state |
24 val define_command: command_id -> string -> state -> state |
24 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state |
25 val edit: version_id -> version_id -> edit list -> header list -> |
|
26 state -> (command_id * exec_id) list * state |
25 val execute: version_id -> state -> state |
27 val execute: version_id -> state -> state |
26 val state: unit -> state |
28 val state: unit -> state |
27 val change_state: (state -> state) -> unit |
29 val change_state: (state -> state) -> unit |
28 end; |
30 end; |
29 |
31 |
75 |
77 |
76 type edit = |
78 type edit = |
77 string * |
79 string * |
78 (*NONE: remove node, SOME: insert/remove commands*) |
80 (*NONE: remove node, SOME: insert/remove commands*) |
79 ((command_id option * command_id option) list) option; |
81 ((command_id option * command_id option) list) option; |
|
82 |
|
83 type header = string * (string * string list * string list); |
80 |
84 |
81 fun the_entry (Node {entries, ...}) id = |
85 fun the_entry (Node {entries, ...}) id = |
82 (case Entries.lookup entries id of |
86 (case Entries.lookup entries id of |
83 NONE => err_undef "command entry" id |
87 NONE => err_undef "command entry" id |
84 | SOME entry => entry); |
88 | SOME entry => entry); |
307 val state' = define_exec exec_id' exec' state; |
311 val state' = define_exec exec_id' exec' state; |
308 in (exec_id', (id, exec_id') :: updates, state') end; |
312 in (exec_id', (id, exec_id') :: updates, state') end; |
309 |
313 |
310 in |
314 in |
311 |
315 |
312 fun edit (old_id: version_id) (new_id: version_id) edits state = |
316 fun edit (old_id: version_id) (new_id: version_id) edits headers state = |
313 let |
317 let |
|
318 (* FIXME apply headers *) |
|
319 |
314 val old_version = the_version state old_id; |
320 val old_version = the_version state old_id; |
315 val _ = Time.now (); (* FIXME odd workaround *) |
321 val _ = Time.now (); (* FIXME odd workaround *) |
316 val new_version = fold edit_nodes edits old_version; |
322 val new_version = fold edit_nodes edits old_version; |
317 |
323 |
318 fun update_node name (rev_updates, version, st) = |
324 fun update_node name (rev_updates, version, st) = |