# HG changeset patch
# User wenzelm
# Date 1287999592 -7200
# Node ID da45a2f45870281eea5ab1d5a41f94ceac5df635
# Parent  fc77d3211f71ef9a8813edc53e10131a50debbf8
removed some remains of Output.debug (follow-up to fce2202892c4);

diff -r fc77d3211f71 -r da45a2f45870 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Oct 25 11:22:30 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Oct 25 11:39:52 2010 +0200
@@ -36,7 +36,6 @@
   val tracing_fn: (output -> unit) Unsynchronized.ref
   val warning_fn: (output -> unit) Unsynchronized.ref
   val error_fn: (output -> unit) Unsynchronized.ref
-  val debug_fn: (output -> unit) Unsynchronized.ref
   val prompt_fn: (output -> unit) Unsynchronized.ref
   val status_fn: (output -> unit) Unsynchronized.ref
   val report_fn: (output -> unit) Unsynchronized.ref
@@ -44,8 +43,6 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
-  val debugging: bool Unsynchronized.ref
-  val debug: (unit -> string) -> unit
 end;
 
 structure Output: OUTPUT =
@@ -93,7 +90,6 @@
 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
 val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
 val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
-val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
 val prompt_fn = Unsynchronized.ref raw_stdout;
 val status_fn = Unsynchronized.ref (fn _: string => ());
 val report_fn = Unsynchronized.ref (fn _: string => ());
@@ -109,9 +105,6 @@
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
-val debugging = Unsynchronized.ref false;
-fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
-
 
 
 (** timing **)