# HG changeset patch # User wenzelm # Date 912341750 -3600 # Node ID 1a2285f3db47e85a7554945b081c8cb070ef78e9 # Parent 389d03e6e09372f490dc1a07dabe04d597e5eed2 replaced wakeup by decorate_prompt_fn; diff -r 389d03e6e093 -r 1a2285f3db47 src/Pure/Syntax/source.ML --- a/src/Pure/Syntax/source.ML Sun Nov 29 13:15:17 1998 +0100 +++ b/src/Pure/Syntax/source.ML Sun Nov 29 13:15:50 1998 +0100 @@ -18,7 +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 decorate_prompt_fn: (string -> 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)) -> @@ -113,10 +113,10 @@ (* stream source *) -val wakeup = ref ""; +val decorate_prompt_fn = ref (fn s:string => s); fun drain_stream instream outstream prompt () = - (TextIO.output (outstream, ! wakeup ^ prompt); + (TextIO.output (outstream, ! decorate_prompt_fn prompt); TextIO.flushOut outstream; (explode (TextIO.inputLine instream), ()));