175 (case get_result node of |
175 (case get_result node of |
176 SOME eval => Command.eval_finished eval |
176 SOME eval => Command.eval_finished eval |
177 | NONE => false); |
177 | NONE => false); |
178 |
178 |
179 fun finished_result_theory node = |
179 fun finished_result_theory node = |
180 finished_result node andalso |
180 if finished_result node then |
181 let val st = Command.eval_result_state (the (get_result node)) |
181 let val st = Command.eval_result_state (the (get_result node)) |
182 in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end; |
182 in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end |
|
183 else NONE; |
183 |
184 |
184 val reset_consolidated = |
185 val reset_consolidated = |
185 map_node (fn (header, keywords, perspective, entries, result, _) => |
186 map_node (fn (header, keywords, perspective, entries, result, _) => |
186 (header, keywords, perspective, entries, result, Lazy.lazy I)); |
187 (header, keywords, perspective, entries, result, Lazy.lazy I)); |
187 |
188 |
188 fun check_consolidated (node as Node {consolidated, ...}) = |
189 fun get_consolidated (Node {consolidated, ...}) = consolidated; |
189 Lazy.is_finished consolidated orelse |
|
190 finished_result_theory node andalso |
|
191 let |
|
192 val result_id = Command.eval_exec_id (the (get_result node)); |
|
193 val eval_ids = |
|
194 iterate_entries (fn (_, opt_exec) => fn eval_ids => |
|
195 (case opt_exec of |
|
196 SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) |
|
197 | NONE => NONE)) node []; |
|
198 in |
|
199 (case Execution.snapshot eval_ids of |
|
200 [] => |
|
201 (Lazy.force consolidated; |
|
202 Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) |
|
203 (fn () => Output.status (Markup.markup_only Markup.consolidated)) (); |
|
204 true) |
|
205 | _ => false) |
|
206 end; |
|
207 |
190 |
208 fun get_node nodes name = String_Graph.get_node nodes name |
191 fun get_node nodes name = String_Graph.get_node nodes name |
209 handle String_Graph.UNDEF _ => empty_node; |
192 handle String_Graph.UNDEF _ => empty_node; |
210 fun default_node name = String_Graph.default_node (name, empty_node); |
193 fun default_node name = String_Graph.default_node (name, empty_node); |
211 fun update_node name f = default_node name #> String_Graph.map_node name f; |
194 fun update_node name f = default_node name #> String_Graph.map_node name f; |
525 val execution' = |
511 val execution' = |
526 {version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; |
512 {version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; |
527 in (versions, blobs, commands, execution') end)); |
513 in (versions, blobs, commands, execution') end)); |
528 |
514 |
529 fun consolidate_execution state = |
515 fun consolidate_execution state = |
530 String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node)) |
516 let |
531 (nodes_of (get_execution_version state)) (); |
517 fun check_consolidated node_name node = |
|
518 if Lazy.is_finished (get_consolidated node) then () |
|
519 else |
|
520 (case finished_result_theory node of |
|
521 NONE => () |
|
522 | SOME thy => |
|
523 let |
|
524 val result_id = Command.eval_exec_id (the (get_result node)); |
|
525 val eval_ids = |
|
526 iterate_entries (fn (_, opt_exec) => fn eval_ids => |
|
527 (case opt_exec of |
|
528 SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) |
|
529 | NONE => NONE)) node []; |
|
530 in |
|
531 (case Execution.snapshot eval_ids of |
|
532 [] => |
|
533 let |
|
534 val (_, offsets, rev_segments) = |
|
535 iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => |
|
536 (case opt_exec of |
|
537 SOME (eval, _) => |
|
538 let |
|
539 val command_id = Command.eval_command_id eval; |
|
540 val span = force_command_span state command_id; |
|
541 |
|
542 val exec_id = Command.eval_exec_id eval; |
|
543 val tr = Command.eval_result_command eval; |
|
544 val st' = Command.eval_result_state eval; |
|
545 |
|
546 val offset' = offset + the_default 0 (Command_Span.symbol_length span); |
|
547 val offsets' = offsets |
|
548 |> Inttab.update (command_id, offset) |
|
549 |> Inttab.update (exec_id, offset); |
|
550 val segments' = (span, tr, st') :: segments; |
|
551 in SOME (offset', offsets', segments') end |
|
552 | NONE => NONE)) node (0, Inttab.empty, []); |
|
553 |
|
554 val adjust = Inttab.lookup offsets; |
|
555 val adjust_pos = Position.adjust_offsets adjust; |
|
556 val adjust_token = Token.adjust_offsets adjust; |
|
557 val segments = |
|
558 rev rev_segments |> map (fn (span, tr, st') => |
|
559 {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); |
|
560 |
|
561 val presentation_context: Thy_Info.presentation_context = |
|
562 {options = Options.default (), |
|
563 file_pos = Position.file node_name, |
|
564 adjust_pos = adjust_pos, |
|
565 segments = segments}; |
|
566 |
|
567 val _ = Lazy.force (get_consolidated node); |
|
568 val _ = |
|
569 Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) |
|
570 (fn () => |
|
571 (if Options.default_bool "editor_document_output" then |
|
572 Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *) |
|
573 else (); |
|
574 Output.status (Markup.markup_only Markup.consolidated))) (); |
|
575 in () end |
|
576 | _ => ()) |
|
577 end); |
|
578 in |
|
579 String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node) |
|
580 (nodes_of (get_execution_version state)) () |
|
581 end; |
532 |
582 |
533 |
583 |
534 |
584 |
535 (** document update **) |
585 (** document update **) |
536 |
586 |
655 val blobs = map (resolve_blob state) blob_digests; |
705 val blobs = map (resolve_blob state) blob_digests; |
656 val span = Lazy.force span0; |
706 val span = Lazy.force span0; |
657 |
707 |
658 val eval' = |
708 val eval' = |
659 Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) |
709 Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) |
660 (blobs, blobs_index) span (#1 (#2 command_exec)); |
710 (blobs, blobs_index) command_id' span (#1 (#2 command_exec)); |
661 val prints' = |
711 val prints' = |
662 perhaps (Command.print command_visible command_overlays keywords command_name eval') []; |
712 perhaps (Command.print command_visible command_overlays keywords command_name eval') []; |
663 val exec' = (eval', prints'); |
713 val exec' = (eval', prints'); |
664 |
714 |
665 val assign_update' = assign_update_new (command_id', SOME exec') assign_update; |
715 val assign_update' = assign_update_new (command_id', SOME exec') assign_update; |