equal
deleted
inserted
replaced
174 |
174 |
175 fun finished_result node = |
175 fun finished_result node = |
176 (case get_result node of |
176 (case get_result node of |
177 SOME eval => Command.eval_finished eval |
177 SOME eval => Command.eval_finished eval |
178 | NONE => false); |
178 | NONE => false); |
179 |
|
180 fun loaded_theory name = |
|
181 get_first Thy_Info.lookup_theory [name, Long_Name.base_name name]; |
|
182 |
179 |
183 fun get_node nodes name = String_Graph.get_node nodes name |
180 fun get_node nodes name = String_Graph.get_node nodes name |
184 handle String_Graph.UNDEF _ => empty_node; |
181 handle String_Graph.UNDEF _ => empty_node; |
185 fun default_node name = String_Graph.default_node (name, empty_node); |
182 fun default_node name = String_Graph.default_node (name, empty_node); |
186 fun update_node name f = default_node name #> String_Graph.map_node name f; |
183 fun update_node name f = default_node name #> String_Graph.map_node name f; |
461 |
458 |
462 val _ = Future.cancel delay_request; |
459 val _ = Future.cancel delay_request; |
463 val delay_request' = Event_Timer.future (Time.now () + delay); |
460 val delay_request' = Event_Timer.future (Time.now () + delay); |
464 |
461 |
465 fun finished_import (name, (node, _)) = |
462 fun finished_import (name, (node, _)) = |
466 finished_result node orelse is_some (loaded_theory name); |
463 finished_result node orelse is_some (Thy_Info.lookup_theory name); |
467 |
464 |
468 val nodes = nodes_of (the_version state version_id); |
465 val nodes = nodes_of (the_version state version_id); |
469 val required = make_required nodes; |
466 val required = make_required nodes; |
470 val _ = |
467 val _ = |
471 nodes |> String_Graph.schedule |
468 nodes |> String_Graph.schedule |
528 fun maybe_end_theory pos st = |
525 fun maybe_end_theory pos st = |
529 SOME (Toplevel.end_theory pos st) |
526 SOME (Toplevel.end_theory pos st) |
530 handle ERROR msg => (Output.error_message msg; NONE); |
527 handle ERROR msg => (Output.error_message msg; NONE); |
531 val parents_reports = |
528 val parents_reports = |
532 imports |> map_filter (fn (import, pos) => |
529 imports |> map_filter (fn (import, pos) => |
533 (case loaded_theory import of |
530 (case Thy_Info.lookup_theory import of |
534 NONE => |
531 NONE => |
535 maybe_end_theory pos |
532 maybe_end_theory pos |
536 (case get_result (snd (the (AList.lookup (op =) deps import))) of |
533 (case get_result (snd (the (AList.lookup (op =) deps import))) of |
537 NONE => Toplevel.toplevel |
534 NONE => Toplevel.toplevel |
538 | SOME eval => Command.eval_result_state eval) |
535 | SOME eval => Command.eval_result_state eval) |
552 val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN; |
549 val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN; |
553 in SOME (Resources.begin_theory master_dir header [parent]) end |
550 in SOME (Resources.begin_theory master_dir header [parent]) end |
554 else NONE; |
551 else NONE; |
555 |
552 |
556 fun check_theory full name node = |
553 fun check_theory full name node = |
557 is_some (loaded_theory name) orelse |
554 is_some (Thy_Info.lookup_theory name) orelse |
558 null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); |
555 null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); |
559 |
556 |
560 fun last_common keywords state node_required node0 node = |
557 fun last_common keywords state node_required node0 node = |
561 let |
558 let |
562 fun update_flags prev (visible, initial) = |
559 fun update_flags prev (visible, initial) = |