equal
deleted
inserted
replaced
26 val init_state: state |
26 val init_state: state |
27 val define_command: command_id -> string -> string -> state -> state |
27 val define_command: command_id -> string -> string -> state -> state |
28 val discontinue_execution: state -> unit |
28 val discontinue_execution: state -> unit |
29 val cancel_execution: state -> Future.task list |
29 val cancel_execution: state -> Future.task list |
30 val execute: version_id -> state -> state |
30 val execute: version_id -> state -> state |
31 val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state |
|
32 val update: version_id -> version_id -> edit list -> state -> |
31 val update: version_id -> version_id -> edit list -> state -> |
33 ((command_id * exec_id option) list * (string * command_id option) list) * state |
32 ((command_id * exec_id option) list * (string * command_id option) list) * state |
34 val remove_versions: version_id list -> state -> state |
33 val remove_versions: version_id list -> state -> state |
35 val state: unit -> state |
34 val state: unit -> state |
36 val change_state: (state -> state) -> unit |
35 val change_state: (state -> state) -> unit |
346 in (versions, commands, (version_id, group, running)) end); |
345 in (versions, commands, (version_id, group, running)) end); |
347 |
346 |
348 |
347 |
349 |
348 |
350 |
349 |
351 (** update **) |
350 (** edits **) |
352 |
351 |
353 (* perspective *) |
352 (* update *) |
354 |
|
355 fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state = |
|
356 let |
|
357 val old_version = the_version state old_id; |
|
358 val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *) |
|
359 val new_version = edit_nodes (name, Perspective perspective) old_version; |
|
360 in define_version new_id new_version state end; |
|
361 |
|
362 |
|
363 (* edits *) |
|
364 |
353 |
365 local |
354 local |
366 |
355 |
367 fun make_required nodes = |
356 fun make_required nodes = |
368 let |
357 let |