src/Pure/Syntax/source.ML

   val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
   val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
   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)) ->
     ('a * 'b list -> 'd * ('a * 'b list)) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source

 val of_file = of_string o File.read;
 
 
 (* 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), ()));
 
 fun of_stream instream outstream =
   make_source [] () default_prompt (drain_stream instream outstream);