equal
deleted
inserted
replaced
127 |
127 |
128 fun output txts stream = List.app (fn txt => TextIO.output (stream, txt)) txts; |
128 fun output txts stream = List.app (fn txt => TextIO.output (stream, txt)) txts; |
129 |
129 |
130 in |
130 in |
131 |
131 |
132 fun read path = |
132 fun read path = CRITICAL (fn () => |
133 fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)); |
133 fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path))); |
134 |
134 |
135 fun write_list path txts = |
135 fun write_list path txts = CRITICAL (fn () => |
136 fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)); |
136 fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path))); |
137 |
137 |
138 fun append_list path txts = |
138 fun append_list path txts = CRITICAL (fn () => |
139 fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)); |
139 fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path))); |
140 |
140 |
141 fun write path txt = write_list path [txt]; |
141 fun write path txt = write_list path [txt]; |
142 fun append path txt = append_list path [txt]; |
142 fun append path txt = append_list path [txt]; |
143 |
143 |
144 end; |
144 end; |