--- a/src/Pure/Tools/debugger.ML Tue Aug 11 13:50:59 2015 +0200
+++ b/src/Pure/Tools/debugger.ML Tue Aug 11 14:13:36 2015 +0200
@@ -185,6 +185,8 @@
(Output.system_message
("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
+in
+
fun debugger_loop thread_name =
uninterruptible (fn restore_attributes => fn () =>
let
@@ -194,19 +196,6 @@
val _ = debugger_state thread_name;
in Exn.release result end) ();
-in
-
-fun init () =
- ML_Debugger.on_breakpoint
- (SOME (fn (_, break) =>
- if not (is_debugging ()) andalso (! break orelse is_stepping ()) andalso
- Options.default_bool @{system_option ML_debugger_active}
- then
- (case Simple_Thread.get_name () of
- SOME thread_name => debugger_loop thread_name
- | NONE => ())
- else ()));
-
end;
@@ -215,7 +204,18 @@
val _ =
Isabelle_Process.protocol_command "Debugger.init"
- (fn [] => init ());
+ (fn [] =>
+ ML_Debugger.on_breakpoint
+ (SOME (fn (_, break) =>
+ if not (is_debugging ()) andalso (! break orelse is_stepping ()) then
+ (case Simple_Thread.get_name () of
+ SOME thread_name => debugger_loop thread_name
+ | NONE => ())
+ else ())));
+
+val _ =
+ Isabelle_Process.protocol_command "Debugger.exit"
+ (fn [] => ML_Debugger.on_breakpoint NONE);
val _ =
Isabelle_Process.protocol_command "Debugger.breakpoint"