# HG changeset patch
# User wenzelm
# Date 1438956953 -7200
# Node ID 20cfa048fe7c1f001e54f6f5ec629020d1a508c1
# Parent  21d70681ec05a1d68c1991b45259a43a41da440d
suppress empty messages as usual;

diff -r 21d70681ec05 -r 20cfa048fe7c src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Fri Aug 07 14:55:35 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Fri Aug 07 16:15:53 2015 +0200
@@ -19,9 +19,11 @@
 val _ = Session.protocol_handler "isabelle.Debugger$Handler";
 
 fun output_message kind msg =
-  Output.protocol_message
-    (Markup.debugger_output (Simple_Thread.the_name ()))
-    [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
+  if msg = "" then ()
+  else
+    Output.protocol_message
+      (Markup.debugger_output (Simple_Thread.the_name ()))
+      [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
 
 val writeln_message = output_message Markup.writelnN;
 val warning_message = output_message Markup.warningN;