# HG changeset patch
# User wenzelm
# Date 1187635440 -7200
# Node ID a0da34cc081ce007a69135b360156dc5b7b1078f
# Parent  44556727197ab441a71b28c299ef225ee679485b
File.read/write/append: non-critical (basic IO operations already thread-safe);

diff -r 44556727197a -r a0da34cc081c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Aug 20 20:43:59 2007 +0200
+++ b/src/Pure/General/file.ML	Mon Aug 20 20:44:00 2007 +0200
@@ -129,14 +129,14 @@
 
 in
 
-fun read path = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
+fun read path =
+  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
 
-fun write_list path txts = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
+fun write_list path txts =
+  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
 
-fun append_list path txts = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
+fun append_list path txts =
+  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];