# HG changeset patch
# User wenzelm
# Date 1439238115 -7200
# Node ID d8d51f956f052ffb0cdc78d1aa16e219699f540e
# Parent  f3039309702e34c0b0b628c74eaeef443878c625
report final debugger_state more robustly, e.g. after interrupt;

diff -r f3039309702e -r d8d51f956f05 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Aug 10 21:11:15 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 22:21:55 2015 +0200
@@ -202,10 +202,13 @@
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
 
 fun debugger_loop thread_name =
-  let
-    fun loop () =
-      (debugger_state thread_name; if debugger_command thread_name then loop () else ());
-  in with_debugging loop; debugger_state thread_name end;
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      fun loop () =
+        (debugger_state thread_name; if debugger_command thread_name then loop () else ());
+      val result = Exn.capture (restore_attributes with_debugging) loop;
+      val _ = debugger_state thread_name;
+    in Exn.release result end) ();
 
 in