# HG changeset patch
# User wenzelm
# Date 897472549 -7200
# Node ID b6363fa0564f6ca831672f3c5a0634f4eda4a725
# Parent  ce8e87fad843fa035f2553fbabe85222bd3c0bf8
added of_file;

diff -r ce8e87fad843 -r b6363fa0564f src/Pure/Syntax/source.ML
--- 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 *)