src/Pure/General/file.ML
changeset 75615 4494cd69f97f
parent 75613 1b50bcd108b7
child 75616 986506233812
equal deleted inserted replaced
75614:01b3da984e55 75615:4494cd69f97f
    18   val rm: Path.T -> unit
    18   val rm: Path.T -> unit
    19   val is_dir: Path.T -> bool
    19   val is_dir: Path.T -> bool
    20   val is_file: Path.T -> bool
    20   val is_file: Path.T -> bool
    21   val check_dir: Path.T -> Path.T
    21   val check_dir: Path.T -> Path.T
    22   val check_file: Path.T -> Path.T
    22   val check_file: Path.T -> Path.T
    23   val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
       
    24   val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
       
    25   val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
       
    26   val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
       
    27   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    23   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    28   val read_dir: Path.T -> string list
    24   val read_dir: Path.T -> string list
    29   val input: BinIO.instream -> string
       
    30   val input_size: int -> BinIO.instream -> string
       
    31   val input_all: BinIO.instream -> string
       
    32   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    25   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    33   val read_lines: Path.T -> string list
    26   val read_lines: Path.T -> string list
    34   val read: Path.T -> string
    27   val read: Path.T -> string
    35   val write: Path.T -> string -> unit
    28   val write: Path.T -> string -> unit
    36   val append: Path.T -> string -> unit
    29   val append: Path.T -> string -> unit
    37   val output: BinIO.outstream -> string -> unit
       
    38   val outputs: BinIO.outstream -> string list -> unit
       
    39   val write_list: Path.T -> string list -> unit
    30   val write_list: Path.T -> string list -> unit
    40   val append_list: Path.T -> string list -> unit
    31   val append_list: Path.T -> string list -> unit
    41   val eq: Path.T * Path.T -> bool
    32   val eq: Path.T * Path.T -> bool
    42 end;
    33 end;
    43 
    34 
    91 fun check_file path =
    82 fun check_file path =
    92   if is_file path then path
    83   if is_file path then path
    93   else error ("No such file: " ^ Path.print (Path.expand path));
    84   else error ("No such file: " ^ Path.print (Path.expand path));
    94 
    85 
    95 
    86 
    96 (* open streams *)
       
    97 
       
    98 local
       
    99 
       
   100 fun with_file open_file close_file f =
       
   101   Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
       
   102     let
       
   103       val file = open_file path;
       
   104       val result = Exn.capture (restore_attributes f) file;
       
   105     in close_file file; Exn.release result end);
       
   106 
       
   107 in
       
   108 
       
   109 fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
       
   110 fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
       
   111 fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
       
   112 fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
       
   113 
       
   114 end;
       
   115 
       
   116 
       
   117 (* directory content *)
    87 (* directory content *)
   118 
    88 
   119 fun fold_dir f path a =
    89 fun fold_dir f path a =
   120   check_dir path |> open_dir (fn stream =>
    90   check_dir path |> File_Stream.open_dir (fn stream =>
   121     let
    91     let
   122       fun read x =
    92       fun read x =
   123         (case OS.FileSys.readDir stream of
    93         (case OS.FileSys.readDir stream of
   124           NONE => x
    94           NONE => x
   125         | SOME entry => read (f entry x));
    95         | SOME entry => read (f entry x));
   126     in read a end);
    96     in read a end);
   127 
    97 
   128 fun read_dir path = sort_strings (fold_dir cons path []);
    98 fun read_dir path = sort_strings (fold_dir cons path []);
   129 
    99 
   130 
   100 
   131 (* input *)
       
   132 
       
   133 val input = Byte.bytesToString o BinIO.input;
       
   134 fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
       
   135 val input_all = Byte.bytesToString o BinIO.inputAll;
       
   136 
       
   137 (*
   101 (*
   138   scalable iterator:
   102   scalable iterator:
   139   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   103   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   140   . optional terminator at end-of-input
   104   . optional terminator at end-of-input
   141 *)
   105 *)
   142 fun fold_lines f path a = open_input (fn file =>
   106 fun fold_lines f path a = File_Stream.open_input (fn file =>
   143   let
   107   let
   144     fun read buf x =
   108     fun read buf x =
   145       (case input file of
   109       (case File_Stream.input file of
   146         "" => (case Buffer.content buf of "" => x | line => f line x)
   110         "" => (case Buffer.content buf of "" => x | line => f line x)
   147       | input =>
   111       | input =>
   148           (case String.fields (fn c => c = #"\n") input of
   112           (case String.fields (fn c => c = #"\n") input of
   149             [rest] => read (Buffer.add rest buf) x
   113             [rest] => read (Buffer.add rest buf) x
   150           | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
   114           | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
   152       | read_more (line :: more) x = read_more more (f line x);
   116       | read_more (line :: more) x = read_more more (f line x);
   153   in read Buffer.empty a end) path;
   117   in read Buffer.empty a end) path;
   154 
   118 
   155 fun read_lines path = rev (fold_lines cons path []);
   119 fun read_lines path = rev (fold_lines cons path []);
   156 
   120 
   157 val read = open_input input_all;
   121 val read = File_Stream.open_input File_Stream.input_all;
   158 
   122 
   159 
   123 
   160 (* output *)
   124 (* write *)
   161 
   125 
   162 fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
   126 fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path;
   163 val outputs = List.app o output;
   127 fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path;
   164 
       
   165 fun output_list txts file = List.app (output file) txts;
       
   166 fun write_list path txts = open_output (output_list txts) path;
       
   167 fun append_list path txts = open_append (output_list txts) path;
       
   168 
   128 
   169 fun write path txt = write_list path [txt];
   129 fun write path txt = write_list path [txt];
   170 fun append path txt = append_list path [txt];
   130 fun append path txt = append_list path [txt];
   171 
   131 
   172 
   132