discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);

--- a/NEWS	Fri Sep 17 21:50:44 2010 +0200
+++ b/NEWS	Fri Sep 17 22:17:57 2010 +0200
@@ -244,6 +244,9 @@
 
 *** ML ***
 
+* Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
+instead (or tracing for high-volume output).
+
 * Configuration option show_question_marks only affects regular pretty
 printing of types and terms, not raw Term.string_of_vname.
 

--- a/src/Pure/General/markup.scala	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/General/markup.scala	Fri Sep 17 22:17:57 2010 +0200
@@ -239,7 +239,6 @@
   val TRACING = "tracing"
   val WARNING = "warning"
   val ERROR = "error"
-  val DEBUG = "debug"
   val SYSTEM = "system"
   val INPUT = "input"
   val STDIN = "stdin"

--- a/src/Pure/Isar/runtime.ML	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 17 22:17:57 2010 +0200
@@ -10,6 +10,7 @@
   exception TERMINATE
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
+  val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
   val exn_messages: (exn -> Position.T) -> exn -> string list
   val exn_message: (exn -> Position.T) -> exn -> string
@@ -28,6 +29,8 @@
 exception EXCURSION_FAIL of exn * string;
 exception TOPLEVEL_ERROR;
 
+val debug = Unsynchronized.ref false;
+
 
 (* exn_context *)
 
@@ -52,7 +55,7 @@
         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
       end;
 
-    val detailed = ! Output.debugging;
+    val detailed = ! debug;
 
     fun exn_msgs context exn =
       if Exn.is_interrupt exn then []
@@ -94,11 +97,10 @@
   | msgs => cat_lines msgs);
 
 
-
 (** controlled execution **)
 
 fun debugging f x =
-  if ! Output.debugging then
+  if ! debug then
     Exn.release (exception_trace (fn () =>
       Exn.Result (f x) handle
         exn as UNDEF => Exn.Exn exn

--- a/src/Pure/Isar/toplevel.ML	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Sep 17 22:17:57 2010 +0200
@@ -215,7 +215,7 @@
 (** toplevel transitions **)
 
 val quiet = Unsynchronized.ref false;
-val debug = Output.debugging;
+val debug = Runtime.debug;
 val interact = Unsynchronized.ref false;
 val timing = Output.timing;
 val profiling = Unsynchronized.ref 0;

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 17 22:17:57 2010 +0200
@@ -79,7 +79,6 @@
   Output.report_fn := (fn _ => ());
   Output.priority_fn := message (special "I") (special "J") "";
   Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.debug_fn := message (special "K") (special "L") "+++ ";
   Output.warning_fn := message (special "K") (special "L") "### ";
   Output.error_fn := message (special "M") (special "N") "*** ";
   Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 17 22:17:57 2010 +0200
@@ -166,8 +166,7 @@
   Output.priority_fn := (fn s => normalmsg Status s);
   Output.tracing_fn := (fn s => normalmsg Tracing s);
   Output.warning_fn := (fn s => errormsg Message Warning s);
-  Output.error_fn := (fn s => errormsg Message Fatal s);
-  Output.debug_fn := (fn s => errormsg Message Debug s));
+  Output.error_fn := (fn s => errormsg Message Fatal s));
 
 
 (* immediate messages *)

--- a/src/Pure/System/isabelle_process.ML	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 17 22:17:57 2010 +0200
@@ -109,7 +109,6 @@
     Output.tracing_fn  := standard_message out_stream true "E";
     Output.warning_fn  := standard_message out_stream true "F";
     Output.error_fn    := standard_message out_stream true "G";
-    Output.debug_fn    := standard_message out_stream true "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     (in_stream, out_stream)

--- a/src/Pure/System/isabelle_process.scala	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri Sep 17 22:17:57 2010 +0200
@@ -28,8 +28,7 @@
       ('D' : Int) -> Markup.WRITELN,
       ('E' : Int) -> Markup.TRACING,
       ('F' : Int) -> Markup.WARNING,
-      ('G' : Int) -> Markup.ERROR,
-      ('H' : Int) -> Markup.DEBUG)
+      ('G' : Int) -> Markup.ERROR)
     def is_raw(kind: String) =
       kind == Markup.STDOUT
     def is_control(kind: String) =

--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 22:17:57 2010 +0200
@@ -6,7 +6,6 @@
 .tracing { background-color: #F0F8FF; }
 .warning { background-color: #EEE8AA; }
 .error { background-color: #FFC1C1; }
-.debug { background-color: #FFE4E1; }
 
 .report { display: none; }
 

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Sep 17 22:17:57 2010 +0200
@@ -32,7 +32,6 @@
   /* component state -- owned by Swing thread */
 
   private var zoom_factor = 100
-  private var show_debug = false
   private var show_tracing = false
   private var follow_caret = true
   private var current_command: Option[Command] = None
@@ -68,8 +67,7 @@
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
                 snapshot.state(cmd).results.iterator.map(_._2) filter {
-                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
-                  case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
+                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
                   case _ => true
                 }
               html_panel.render(filtered_results.toList)
@@ -122,13 +120,6 @@
   private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   zoom.tooltip = "Zoom factor for basic font size"
 
-  private val debug = new CheckBox("Debug") {
-    reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
-  }
-  debug.selected = show_debug
-  debug.tooltip =
-    "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
-
   private val tracing = new CheckBox("Tracing") {
     reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   }
@@ -146,7 +137,7 @@
   }
   update.tooltip = "Update display according to the command at cursor position"
 
-  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
+  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
   add(controls.peer, BorderLayout.NORTH)
 
   handle_update()