src/Pure/General/output.ML

--- a/src/Pure/General/output.ML	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Pure/General/output.ML	Fri Sep 28 16:51:58 2012 +0200
@@ -43,6 +43,7 @@
   val status: string -> unit
   val report: string -> unit
   val protocol_message: Properties.T -> string -> unit
+  exception TRACING_LIMIT of int
 end;
 
 structure Output: OUTPUT =
@@ -111,6 +112,8 @@
 fun report s = ! Private_Hooks.report_fn (output s);
 fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
+exception TRACING_LIMIT of int;
+
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;