src/Pure/Thy/file.ML
changeset 4216 419113535e48
child 4341 4adf0b093275
equal deleted inserted replaced
4215:7f7519759b8c 4216:419113535e48
       
     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;