equal
deleted
inserted
replaced
12 val info: string -> string |
12 val info: string -> string |
13 val read: string -> string |
13 val read: string -> string |
14 val write: string -> string -> unit |
14 val write: string -> string -> unit |
15 val append: string -> string -> unit |
15 val append: string -> string -> unit |
16 val copy: string -> string -> unit |
16 val copy: string -> string -> unit |
|
17 val source: string -> (string, string list) Source.source |
17 end; |
18 end; |
18 |
19 |
19 structure File: FILE = |
20 structure File: FILE = |
20 struct |
21 struct |
21 |
22 |
58 |
59 |
59 fun copy infile outfile = |
60 fun copy infile outfile = |
60 if not (exists infile) then error ("File not found: " ^ quote infile) |
61 if not (exists infile) then error ("File not found: " ^ quote infile) |
61 else write outfile (read infile); |
62 else write outfile (read infile); |
62 |
63 |
|
64 val source = Source.of_string o read; |
|
65 |
63 |
66 |
64 end; |
67 end; |