tty: issue wakeup;
authorwenzelm
Sat Nov 21 12:16:41 1998 +0100 (1998-11-21)
changeset 5943576a7f5e5e39
parent 5942 9a7bf515fde1
child 5944 dcc446da8e19
tty: issue wakeup;
src/Pure/Syntax/source.ML
     1.1 --- a/src/Pure/Syntax/source.ML	Sat Nov 21 12:16:15 1998 +0100
     1.2 +++ b/src/Pure/Syntax/source.ML	Sat Nov 21 12:16:41 1998 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val of_list: 'a list -> ('a, 'a list) source
     1.5    val of_string: string -> (string, string list) source
     1.6    val of_file: string -> (string, string list) source
     1.7 +  val wakeup: string ref
     1.8    val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
     1.9    val tty: (string, unit) source
    1.10    val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    1.11 @@ -112,8 +113,10 @@
    1.12  
    1.13  (* stream source *)
    1.14  
    1.15 +val wakeup = ref "";
    1.16 +
    1.17  fun drain_stream instream outstream prompt () =
    1.18 -  (TextIO.output (outstream, prompt);
    1.19 +  (TextIO.output (outstream, ! wakeup ^ prompt);
    1.20      TextIO.flushOut outstream;
    1.21      (explode (TextIO.inputLine instream), ()));
    1.22