# HG changeset patch
# User wenzelm
# Date 895590868 -7200
# Node ID a1b5d156ec33ce3ca5d93192a9211cadc534f434
# Parent  067533f8c41972079ba7e62f543f978aeb309806
added source: string -> (string, string list) Source.source;

diff -r 067533f8c419 -r a1b5d156ec33 src/Pure/Thy/file.ML
--- a/src/Pure/Thy/file.ML	Tue May 19 17:14:01 1998 +0200
+++ b/src/Pure/Thy/file.ML	Tue May 19 17:14:28 1998 +0200
@@ -14,6 +14,7 @@
   val write: string -> string -> unit
   val append: string -> string -> unit
   val copy: string -> string -> unit
+  val source: string -> (string, string list) Source.source
 end;
 
 structure File: FILE =
@@ -60,5 +61,7 @@
   if not (exists infile) then error ("File not found: " ^ quote infile)
   else write outfile (read infile);
 
+val source = Source.of_string o read;
+
 
 end;