Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
before close: Exn.capture/release;
authorwenzelm
Mon, 31 Mar 2008 23:08:55 +0200
changeset 26504 6e87c0a60104
parent 26503 4dec4460244f
child 26505 49967f8b1068
before close: Exn.capture/release;
src/Pure/ML-Systems/alice.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/mosml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/multithreading_polyml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml_old_compiler4.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml_old_compiler5.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/system_shell.ML file | annotate | diff | comparison | revisions 
--- 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
 
--- 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
 
--- 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 *)
--- 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;
 
--- 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;
 
--- 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;
 
--- 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 =
--- 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
isabelle