src/Pure/General/file.ML
changeset 56533 cd8b6d849b6a
parent 48911 5debc3e4fa81
child 59058 a78612c67ec0
equal deleted inserted replaced
56532:3da244bc02bd 56533:cd8b6d849b6a
    33   val append: Path.T -> string -> unit
    33   val append: Path.T -> string -> unit
    34   val write_list: Path.T -> string list -> unit
    34   val write_list: Path.T -> string list -> unit
    35   val append_list: Path.T -> string list -> unit
    35   val append_list: Path.T -> string list -> unit
    36   val write_buffer: Path.T -> Buffer.T -> unit
    36   val write_buffer: Path.T -> Buffer.T -> unit
    37   val eq: Path.T * Path.T -> bool
    37   val eq: Path.T * Path.T -> bool
    38   val copy: Path.T -> Path.T -> unit
       
    39 end;
    38 end;
    40 
    39 
    41 structure File: FILE =
    40 structure File: FILE =
    42 struct
    41 struct
    43 
    42 
   163 fun append path txt = append_list path [txt];
   162 fun append path txt = append_list path [txt];
   164 
   163 
   165 fun write_buffer path buf = open_output (Buffer.output buf) path;
   164 fun write_buffer path buf = open_output (Buffer.output buf) path;
   166 
   165 
   167 
   166 
   168 (* copy *)
   167 (* eq *)
   169 
   168 
   170 fun eq paths =
   169 fun eq paths =
   171   (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
   170   (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
   172     SOME ids => is_equal (OS.FileSys.compare ids)
   171     SOME ids => is_equal (OS.FileSys.compare ids)
   173   | NONE => false);
   172   | NONE => false);
   174 
   173 
   175 fun copy src dst =
       
   176   if eq (src, dst) then ()
       
   177   else
       
   178     let val target = if is_dir dst then Path.append dst (Path.base src) else dst
       
   179     in write target (read src) end;
       
   180 
       
   181 end;
   174 end;