--- a/src/Pure/Syntax/source.ML Wed Jun 10 11:55:30 1998 +0200
+++ b/src/Pure/Syntax/source.ML Wed Jun 10 11:55:49 1998 +0200
@@ -17,6 +17,7 @@
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 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)) ->
@@ -106,6 +107,7 @@
fun of_list xs = make_source [] xs default_prompt drain_list;
val of_string = of_list o explode;
+val of_file = of_string o File.read;
(* stream source *)