# HG changeset patch
# User wenzelm
# Date 911647001 -3600
# Node ID 576a7f5e5e3984469baca2233413b691114a8d71
# Parent  9a7bf515fde197cffe98409cdbc1a7ff5faa6b5a
tty: issue wakeup;

diff -r 9a7bf515fde1 -r 576a7f5e5e39 src/Pure/Syntax/source.ML
--- a/src/Pure/Syntax/source.ML	Sat Nov 21 12:16:15 1998 +0100
+++ b/src/Pure/Syntax/source.ML	Sat Nov 21 12:16:41 1998 +0100
@@ -18,6 +18,7 @@
   val of_list: 'a list -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
   val of_file: string -> (string, string list) source
+  val wakeup: string ref
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
@@ -112,8 +113,10 @@
 
 (* stream source *)
 
+val wakeup = ref "";
+
 fun drain_stream instream outstream prompt () =
-  (TextIO.output (outstream, prompt);
+  (TextIO.output (outstream, ! wakeup ^ prompt);
     TextIO.flushOut outstream;
     (explode (TextIO.inputLine instream), ()));