equal
deleted
inserted
replaced
360 |> Thm.join_theory_proofs) ())); |
360 |> Thm.join_theory_proofs) ())); |
361 |
361 |
362 fun stable_command exec = |
362 fun stable_command exec = |
363 (case Exn.capture Command.memo_result exec of |
363 (case Exn.capture Command.memo_result exec of |
364 Exn.Exn exn => not (Exn.is_interrupt exn) |
364 Exn.Exn exn => not (Exn.is_interrupt exn) |
365 | Exn.Res ((st, _), _) => |
365 | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st))); |
366 (case try Toplevel.theory_of st of |
|
367 NONE => true |
|
368 | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy)))); |
|
369 |
366 |
370 fun make_required nodes = |
367 fun make_required nodes = |
371 let |
368 let |
372 val all_visible = |
369 val all_visible = |
373 Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] |
370 Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] |