# HG changeset patch
# User wenzelm
# Date 1199631471 -3600
# Node ID c448a5f15f31152aeb84df2aba0cdf7af6292b99
# Parent  8943e72bf92ac8720c6b17dc00d063e2131ddf1a
added explicit prompt channel (prompt_fn/prompt);
tuned;

diff -r 8943e72bf92a -r c448a5f15f31 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sun Jan 06 15:57:49 2008 +0100
+++ b/src/Pure/General/output.ML	Sun Jan 06 15:57:51 2008 +0100
@@ -41,10 +41,12 @@
   val warning_fn: (output -> unit) ref
   val error_fn: (output -> unit) ref
   val debug_fn: (output -> unit) ref
+  val prompt_fn: (output -> unit) ref
+  val error_msg: string -> unit
+  val prompt: string -> unit
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
-  val error_msg: string -> unit
   val ml_output: (string -> unit) * (string -> 'a)
   val accumulated_time: unit -> unit
 end;
@@ -98,11 +100,14 @@
 val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
 val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
 val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = ref std_output;
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
 fun tracing s = ! tracing_fn (output s);
 fun warning s = ! warning_fn (output s);
+fun error_msg s = ! error_fn (output s);
+fun prompt s = ! prompt_fn (output s);
 
 val tolerate_legacy_features = ref true;
 fun legacy_feature s =
@@ -113,8 +118,6 @@
 val debugging = ref false;
 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
 
-fun error_msg s = ! error_fn (output s);
-
 val ml_output = (writeln, error);