report final debugger_state more robustly, e.g. after interrupt;

--- 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