1.1 --- a/src/Pure/ML-Systems/alice.ML	Mon Mar 31 23:08:54 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Mar 31 23:08:55 2008 +0200
     1.3 @@ -152,11 +152,11 @@
     1.4  
     1.5  fun read_file name =
     1.6    let val is = TextIO.openIn name
     1.7 -  in TextIO.inputAll is before TextIO.closeIn is end;
     1.8 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
     1.9  
    1.10  fun write_file name txt =
    1.11    let val os = TextIO.openOut name
    1.12 -  in TextIO.output (os, txt) before TextIO.closeOut os end;
    1.13 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    1.14  
    1.15  in
    1.16  

     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Mon Mar 31 23:08:54 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Mar 31 23:08:55 2008 +0200
     2.3 @@ -193,11 +193,11 @@
     2.4  
     2.5  fun read_file name =
     2.6    let val is = TextIO.openIn name
     2.7 -  in TextIO.inputAll is before TextIO.closeIn is end;
     2.8 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
     2.9  
    2.10  fun write_file name txt =
    2.11    let val os = TextIO.openOut name
    2.12 -  in TextIO.output (os, txt) before TextIO.closeOut os end;
    2.13 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    2.14  
    2.15  in
    2.16  

     3.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Mar 31 23:08:54 2008 +0200
     3.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Mar 31 23:08:55 2008 +0200
     3.3 @@ -62,11 +62,11 @@
     3.4  
     3.5  fun read_file name =
     3.6    let val is = TextIO.openIn name
     3.7 -  in TextIO.inputAll is before TextIO.closeIn is end;
     3.8 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
     3.9  
    3.10  fun write_file name txt =
    3.11    let val os = TextIO.openOut name
    3.12 -  in TextIO.output (os, txt) before TextIO.closeOut os end;
    3.13 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    3.14  
    3.15  
    3.16  (* thread attributes *)

     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 31 23:08:54 2008 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 31 23:08:55 2008 +0200
     4.3 @@ -39,6 +39,6 @@
     4.4  fun use_file tune output verbose name =
     4.5    let
     4.6      val instream = TextIO.openIn name;
     4.7 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     4.8 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     4.9    in use_text tune (1, name) output verbose txt end;
    4.10  

     5.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:54 2008 +0200
     5.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 31 23:08:55 2008 +0200
     5.3 @@ -29,6 +29,6 @@
     5.4  fun use_file tune output verbose name =
     5.5    let
     5.6      val instream = TextIO.openIn name;
     5.7 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     5.8 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     5.9    in use_text tune (1, name) output verbose txt end;
    5.10  

     6.1 --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 31 23:08:54 2008 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 31 23:08:55 2008 +0200
     6.3 @@ -29,6 +29,6 @@
     6.4  fun use_file tune output verbose name =
     6.5    let
     6.6      val instream = TextIO.openIn name;
     6.7 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     6.8 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     6.9    in use_text tune (1, name) output verbose txt end;
    6.10  

     7.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:54 2008 +0200
     7.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 31 23:08:55 2008 +0200
     7.3 @@ -132,7 +132,7 @@
     7.4  fun use_file tune output verbose name =
     7.5    let
     7.6      val instream = TextIO.openIn name;
     7.7 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     7.8 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     7.9    in use_text tune (1, name) output verbose txt end;
    7.10  
    7.11  fun forget_structure name =

     8.1 --- a/src/Pure/ML-Systems/system_shell.ML	Mon Mar 31 23:08:54 2008 +0200
     8.2 +++ b/src/Pure/ML-Systems/system_shell.ML	Mon Mar 31 23:08:55 2008 +0200
     8.3 @@ -10,11 +10,11 @@
     8.4  
     8.5  fun read_file name =
     8.6    let val is = TextIO.openIn name
     8.7 -  in TextIO.inputAll is before TextIO.closeIn is end;
     8.8 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
     8.9  
    8.10  fun write_file name txt =
    8.11    let val os = TextIO.openOut name
    8.12 -  in TextIO.output (os, txt) before TextIO.closeOut os end;
    8.13 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    8.14  
    8.15  in
    8.16