# HG changeset patch
# User wenzelm
# Date 1284754677 -7200
# Node ID fce2202892c495eac2cfffeb7c55484d60db052b
# Parent  31290f54be1961dccc8b633159f46323ae5e728c
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);

diff -r 31290f54be19 -r fce2202892c4 NEWS
--- 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.
 
diff -r 31290f54be19 -r fce2202892c4 src/Pure/General/markup.scala
--- 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"
diff -r 31290f54be19 -r fce2202892c4 src/Pure/Isar/runtime.ML
--- 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
diff -r 31290f54be19 -r fce2202892c4 src/Pure/Isar/toplevel.ML
--- 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;
diff -r 31290f54be19 -r fce2202892c4 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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")));
diff -r 31290f54be19 -r fce2202892c4 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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 *)
diff -r 31290f54be19 -r fce2202892c4 src/Pure/System/isabelle_process.ML
--- 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)
diff -r 31290f54be19 -r fce2202892c4 src/Pure/System/isabelle_process.scala
--- 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) =
diff -r 31290f54be19 -r fce2202892c4 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- 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; }
 
diff -r 31290f54be19 -r fce2202892c4 src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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()