27 val define_command: command_id -> string -> string -> state -> state |
27 val define_command: command_id -> string -> string -> state -> state |
28 val remove_versions: version_id list -> state -> state |
28 val remove_versions: version_id list -> state -> state |
29 val discontinue_execution: state -> unit |
29 val discontinue_execution: state -> unit |
30 val cancel_execution: state -> unit |
30 val cancel_execution: state -> unit |
31 val start_execution: state -> unit |
31 val start_execution: state -> unit |
|
32 val timing: bool Unsynchronized.ref |
32 val update: version_id -> version_id -> edit list -> state -> |
33 val update: version_id -> version_id -> edit list -> state -> |
33 (command_id * exec_id option) list * state |
34 (command_id * exec_id option) list * state |
34 val state: unit -> state |
35 val state: unit -> state |
35 val change_state: (state -> state) -> unit |
36 val change_state: (state -> state) -> unit |
36 end; |
37 end; |
445 |
449 |
446 fun update (old_id: version_id) (new_id: version_id) edits state = |
450 fun update (old_id: version_id) (new_id: version_id) edits state = |
447 let |
451 let |
448 val old_version = the_version state old_id; |
452 val old_version = the_version state old_id; |
449 val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) |
453 val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) |
450 val new_version = fold edit_nodes edits old_version; |
454 val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); |
451 |
455 |
452 val nodes = nodes_of new_version; |
456 val nodes = nodes_of new_version; |
453 val is_required = make_required nodes; |
457 val is_required = make_required nodes; |
454 |
458 |
455 val _ = terminate_execution state; |
459 val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state); |
456 val updated = |
460 val updated = timeit "Document.update" (fn () => |
457 nodes |> Graph.schedule |
461 nodes |> Graph.schedule |
458 (fn deps => fn (name, node) => |
462 (fn deps => fn (name, node) => |
459 (singleton o Future.forks) |
463 (singleton o Future.forks) |
460 {name = "Document.update", group = NONE, |
464 {name = "Document.update", group = NONE, |
461 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
465 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
509 if null no_execs andalso null new_execs then NONE |
513 if null no_execs andalso null new_execs then NONE |
510 else SOME (name, node'); |
514 else SOME (name, node'); |
511 in ((no_execs, new_execs, updated_node), node') end |
515 in ((no_execs, new_execs, updated_node), node') end |
512 else (([], [], NONE), node) |
516 else (([], [], NONE), node) |
513 end)) |
517 end)) |
514 |> Future.joins |> map #1; |
518 |> Future.joins |> map #1); |
515 |
519 |
516 val command_execs = |
520 val command_execs = |
517 map (rpair NONE) (maps #1 updated) @ |
521 map (rpair NONE) (maps #1 updated) @ |
518 map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); |
522 map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); |
519 val updated_nodes = map_filter #3 updated; |
523 val updated_nodes = map_filter #3 updated; |