|
1 (* Title: Pure/Thy/file.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 File system operations. |
|
6 *) |
|
7 |
|
8 signature BASIC_FILE = |
|
9 sig |
|
10 val maketest: string -> unit |
|
11 end; |
|
12 |
|
13 signature FILE = |
|
14 sig |
|
15 include BASIC_FILE |
|
16 val exists: string -> bool |
|
17 val read: string -> string |
|
18 val write: string -> string -> unit |
|
19 val append: string -> string -> unit |
|
20 val copy: string -> string -> unit |
|
21 end; |
|
22 |
|
23 structure File: FILE = |
|
24 struct |
|
25 |
|
26 |
|
27 (* exists *) |
|
28 |
|
29 fun exists name = (file_info name <> ""); |
|
30 |
|
31 |
|
32 (* read / write files *) |
|
33 |
|
34 fun read name = |
|
35 let |
|
36 val instream = TextIO.openIn name; |
|
37 val intext = TextIO.inputAll instream; |
|
38 in |
|
39 TextIO.closeIn instream; |
|
40 intext |
|
41 end; |
|
42 |
|
43 fun write name txt = |
|
44 let val outstream = TextIO.openOut name in |
|
45 TextIO.output (outstream, txt); |
|
46 TextIO.closeOut outstream |
|
47 end; |
|
48 |
|
49 fun append name txt = |
|
50 let val outstream = TextIO.openAppend name in |
|
51 TextIO.output (outstream, txt); |
|
52 TextIO.closeOut outstream |
|
53 end; |
|
54 |
|
55 fun copy infile outfile = (* FIXME improve *) |
|
56 if not (exists infile) then error ("File not found: " ^ quote infile) |
|
57 else write outfile (read infile); |
|
58 |
|
59 |
|
60 (*for the "test" target in IsaMakefiles -- signifies successful termination*) |
|
61 fun maketest msg = |
|
62 (writeln msg; write "test" "Test examples ran successfully\n"); |
|
63 |
|
64 |
|
65 end; |
|
66 |
|
67 |
|
68 structure BasicFile: BASIC_FILE = File; |
|
69 open BasicFile; |