equal
deleted
inserted
replaced
274 (case Document.command_exec (Document.state ()) node_name id of |
274 (case Document.command_exec (Document.state ()) node_name id of |
275 SOME (eval, _) => |
275 SOME (eval, _) => |
276 if Command.eval_finished eval then |
276 if Command.eval_finished eval then |
277 let |
277 let |
278 val st = Command.eval_result_state eval; |
278 val st = Command.eval_result_state eval; |
279 val ctxt = Toplevel.presentation_context_of st |
279 val ctxt = Toplevel.presentation_context st |
280 handle Toplevel.UNDEF => err (); |
280 handle Toplevel.UNDEF => err (); |
281 in |
281 in |
282 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of |
282 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of |
283 SOME (b, _) => b := breakpoint_state |
283 SOME (b, _) => b := breakpoint_state |
284 | NONE => err ()) |
284 | NONE => err ()) |