# HG changeset patch
# User wenzelm
# Date 1206997735 -7200
# Node ID 6e87c0a6010412b5e645a2068daa3424f8d54012
# Parent  4dec4460244f3af309e3f71247025f046218a652
before close: Exn.capture/release;

diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -152,11 +152,11 @@
 
 fun read_file name =
   let val is = TextIO.openIn name
-  in TextIO.inputAll is before TextIO.closeIn is end;
+  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
 
 fun write_file name txt =
   let val os = TextIO.openOut name
-  in TextIO.output (os, txt) before TextIO.closeOut os end;
+  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
 
 in
 
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -193,11 +193,11 @@
 
 fun read_file name =
   let val is = TextIO.openIn name
-  in TextIO.inputAll is before TextIO.closeIn is end;
+  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
 
 fun write_file name txt =
   let val os = TextIO.openOut name
-  in TextIO.output (os, txt) before TextIO.closeOut os end;
+  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
 
 in
 
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -62,11 +62,11 @@
 
 fun read_file name =
   let val is = TextIO.openIn name
-  in TextIO.inputAll is before TextIO.closeIn is end;
+  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
 
 fun write_file name txt =
   let val os = TextIO.openOut name
-  in TextIO.output (os, txt) before TextIO.closeOut os end;
+  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
 
 
 (* thread attributes *)
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -39,6 +39,6 @@
 fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
-    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune (1, name) output verbose txt end;
 
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -29,6 +29,6 @@
 fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
-    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune (1, name) output verbose txt end;
 
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/polyml_old_compiler5.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -29,6 +29,6 @@
 fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
-    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune (1, name) output verbose txt end;
 
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -132,7 +132,7 @@
 fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
-    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text tune (1, name) output verbose txt end;
 
 fun forget_structure name =
diff -r 4dec4460244f -r 6e87c0a60104 src/Pure/ML-Systems/system_shell.ML
--- a/src/Pure/ML-Systems/system_shell.ML	Mon Mar 31 23:08:54 2008 +0200
+++ b/src/Pure/ML-Systems/system_shell.ML	Mon Mar 31 23:08:55 2008 +0200
@@ -10,11 +10,11 @@
 
 fun read_file name =
   let val is = TextIO.openIn name
-  in TextIO.inputAll is before TextIO.closeIn is end;
+  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
 
 fun write_file name txt =
   let val os = TextIO.openOut name
-  in TextIO.output (os, txt) before TextIO.closeOut os end;
+  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
 
 in