--- a/src/Pure/General/file.ML Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/file.ML Mon Jul 23 14:06:12 2007 +0200
@@ -129,14 +129,14 @@
in
-fun read path =
- fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
+fun read path = CRITICAL (fn () =>
+ fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
-fun write_list path txts =
- fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
+fun write_list path txts = CRITICAL (fn () =>
+ fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
-fun append_list path txts =
- fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
+fun append_list path txts = CRITICAL (fn () =>
+ fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
fun write path txt = write_list path [txt];
fun append path txt = append_list path [txt];