src/Pure/Tools/debugger.ML
changeset 67381 146757999c8d
parent 65222 fb8253564483
child 68816 5a53724fe247
equal deleted inserted replaced
67380:8bef51521f21 67381:146757999c8d
   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 ())