replaced wakeup by decorate_prompt_fn;
authorwenzelm
Sun Nov 29 13:15:50 1998 +0100 (1998-11-29)
changeset 59881a2285f3db47
parent 5987 389d03e6e093
child 5989 9670dae0143d
replaced wakeup by decorate_prompt_fn;
src/Pure/Syntax/source.ML
     1.1 --- a/src/Pure/Syntax/source.ML	Sun Nov 29 13:15:17 1998 +0100
     1.2 +++ b/src/Pure/Syntax/source.ML	Sun Nov 29 13:15:50 1998 +0100
     1.3 @@ -18,7 +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 decorate_prompt_fn: (string -> string) ref
     1.9    val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
    1.10    val tty: (string, unit) source
    1.11    val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    1.12 @@ -113,10 +113,10 @@
    1.13  
    1.14  (* stream source *)
    1.15  
    1.16 -val wakeup = ref "";
    1.17 +val decorate_prompt_fn = ref (fn s:string => s);
    1.18  
    1.19  fun drain_stream instream outstream prompt () =
    1.20 -  (TextIO.output (outstream, ! wakeup ^ prompt);
    1.21 +  (TextIO.output (outstream, ! decorate_prompt_fn prompt);
    1.22      TextIO.flushOut outstream;
    1.23      (explode (TextIO.inputLine instream), ()));
    1.24