25 type state |
25 type state |
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 update_perspective: version_id -> version_id -> string -> command_id list -> state -> state |
31 val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state |
31 val update: version_id -> version_id -> edit list -> state -> |
32 val update: version_id -> version_id -> edit list -> state -> |
32 ((command_id * exec_id option) list * (string * command_id option) list) * state |
33 ((command_id * exec_id option) list * (string * command_id option) list) * state |
33 val execute: version_id -> state -> state |
|
34 val remove_versions: version_id list -> state -> state |
34 val remove_versions: version_id list -> state -> state |
35 val state: unit -> state |
35 val state: unit -> state |
36 val change_state: (state -> state) -> unit |
36 val change_state: (state -> state) -> unit |
37 end; |
37 end; |
38 |
38 |
108 |
108 |
109 fun get_perspective (Node {perspective, ...}) = perspective; |
109 fun get_perspective (Node {perspective, ...}) = perspective; |
110 fun set_perspective ids = |
110 fun set_perspective ids = |
111 map_node (fn (touched, header, _, entries, last_exec, result) => |
111 map_node (fn (touched, header, _, entries, last_exec, result) => |
112 (touched, header, make_perspective ids, entries, last_exec, result)); |
112 (touched, header, make_perspective ids, entries, last_exec, result)); |
|
113 |
|
114 val visible_command = #1 o get_perspective; |
|
115 val visible_last = #2 o get_perspective; |
|
116 val visible_node = is_some o visible_last |
113 |
117 |
114 fun map_entries f = |
118 fun map_entries f = |
115 map_node (fn (touched, header, perspective, entries, last_exec, result) => |
119 map_node (fn (touched, header, perspective, entries, last_exec, result) => |
116 (touched, header, perspective, f entries, last_exec, result)); |
120 (touched, header, perspective, f entries, last_exec, result)); |
117 fun get_entries (Node {entries, ...}) = entries; |
121 fun get_entries (Node {entries, ...}) = entries; |
291 | SOME command => command); |
295 | SOME command => command); |
292 |
296 |
293 |
297 |
294 (* document execution *) |
298 (* document execution *) |
295 |
299 |
296 fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; |
300 fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; |
297 |
301 |
298 fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group; |
302 fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group; |
299 |
303 |
300 end; |
304 end; |
|
305 |
|
306 |
|
307 |
|
308 (** execute **) |
|
309 |
|
310 fun finished_theory node = |
|
311 (case Exn.capture Command.memo_result (get_result node) of |
|
312 Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st |
|
313 | _ => false); |
|
314 |
|
315 fun execute version_id state = |
|
316 state |> map_state (fn (versions, commands, _) => |
|
317 let |
|
318 val version = the_version state version_id; |
|
319 |
|
320 val group = Future.new_group NONE; |
|
321 val running = Unsynchronized.ref true; |
|
322 |
|
323 fun run _ _ NONE = () |
|
324 | run node command_id (SOME (_, exec)) = |
|
325 let |
|
326 val (_, print) = Command.memo_eval exec; |
|
327 val _ = |
|
328 if visible_command node command_id |
|
329 then ignore (Lazy.future Future.default_params print) |
|
330 else (); |
|
331 in () end; |
|
332 |
|
333 val _ = |
|
334 nodes_of version |> Graph.schedule |
|
335 (fn deps => fn (name, node) => |
|
336 if not (visible_node node) andalso finished_theory node then |
|
337 Future.value () |
|
338 else |
|
339 (singleton o Future.forks) |
|
340 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), |
|
341 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} |
|
342 (fn () => |
|
343 iterate_entries (fn ((_, id), exec) => fn () => |
|
344 if ! running then SOME (run node id exec) else NONE) node ())); |
|
345 |
|
346 in (versions, commands, (version_id, group, running)) end); |
|
347 |
301 |
348 |
302 |
349 |
303 |
350 |
304 (** update **) |
351 (** update **) |
305 |
352 |
318 local |
365 local |
319 |
366 |
320 fun make_required nodes = |
367 fun make_required nodes = |
321 let |
368 let |
322 val all_visible = |
369 val all_visible = |
323 Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes [] |
370 Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] |
324 |> Graph.all_preds nodes; |
371 |> Graph.all_preds nodes |
|
372 |> map (rpair ()) |> Symtab.make; |
|
373 |
325 val required = |
374 val required = |
326 fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ())) |
375 Symtab.fold (fn (a, ()) => |
327 all_visible Symtab.empty; |
376 exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? |
|
377 Symtab.update (a, ())) all_visible Symtab.empty; |
328 in Symtab.defined required end; |
378 in Symtab.defined required end; |
329 |
379 |
330 fun init_theory deps node = |
380 fun init_theory deps node = |
331 let |
381 let |
332 (* FIXME provide files via Scala layer, not master_dir *) |
382 (* FIXME provide files via Scala layer, not master_dir *) |
417 val is_required = make_required nodes; |
467 val is_required = make_required nodes; |
418 |
468 |
419 val updated = |
469 val updated = |
420 nodes |> Graph.schedule |
470 nodes |> Graph.schedule |
421 (fn deps => fn (name, node) => |
471 (fn deps => fn (name, node) => |
422 if is_touched node orelse is_required name then |
472 if is_touched node orelse is_required name andalso not (finished_theory node) then |
423 let |
473 let |
424 val node0 = node_of old_version name; |
474 val node0 = node_of old_version name; |
425 fun init () = init_theory deps node; |
475 fun init () = init_theory deps node; |
426 val bad_init = |
476 val bad_init = |
427 not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); |
477 not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); |
430 {name = "Document.update", group = NONE, |
480 {name = "Document.update", group = NONE, |
431 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
481 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} |
432 (fn () => |
482 (fn () => |
433 let |
483 let |
434 val required = is_required name; |
484 val required = is_required name; |
435 val last_visible = #2 (get_perspective node); |
485 val last_visible = visible_last node; |
436 val (common, (visible, initial)) = last_common state last_visible node0 node; |
486 val (common, (visible, initial)) = last_common state last_visible node0 node; |
437 val common_command_exec = the_default_entry node common; |
487 val common_command_exec = the_default_entry node common; |
438 |
488 |
439 val (execs, (command_id, (_, exec)), _) = |
489 val (execs, (command_id, (_, exec)), _) = |
440 ([], common_command_exec, if initial then SOME init else NONE) |> |
490 ([], common_command_exec, if initial then SOME init else NONE) |> |
478 in ((command_execs, last_execs), state') end; |
528 in ((command_execs, last_execs), state') end; |
479 |
529 |
480 end; |
530 end; |
481 |
531 |
482 |
532 |
483 (* execute *) |
|
484 |
|
485 fun execute version_id state = |
|
486 state |> map_state (fn (versions, commands, _) => |
|
487 let |
|
488 val version = the_version state version_id; |
|
489 |
|
490 val group = Future.new_group NONE; |
|
491 val running = Unsynchronized.ref true; |
|
492 |
|
493 fun run _ _ NONE = () |
|
494 | run node command_id (SOME (_, exec)) = |
|
495 let |
|
496 val (_, print) = Command.memo_eval exec; |
|
497 val _ = |
|
498 if #1 (get_perspective node) command_id |
|
499 then ignore (Lazy.future Future.default_params print) |
|
500 else (); |
|
501 in () end; |
|
502 |
|
503 val _ = |
|
504 nodes_of version |> Graph.schedule |
|
505 (fn deps => fn (name, node) => |
|
506 (singleton o Future.forks) |
|
507 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), |
|
508 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} |
|
509 (fn () => |
|
510 iterate_entries (fn ((_, id), exec) => fn () => |
|
511 if ! running then SOME (run node id exec) else NONE) node ())); |
|
512 |
|
513 in (versions, commands, (version_id, group, running)) end); |
|
514 |
|
515 |
|
516 (* remove versions *) |
533 (* remove versions *) |
517 |
534 |
518 fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => |
535 fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => |
519 let |
536 let |
520 val _ = member (op =) ids (#1 execution) andalso |
537 val _ = member (op =) ids (#1 execution) andalso |