# 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