improved error behaviour of use (bootstrap version);
authorwenzelm
Thu, 20 Sep 2007 17:48:16 +0200
changeset 24663 015a8838e656
parent 24662 f79f6061525c
child 24664 4195de64fdb1
improved error behaviour of use (bootstrap version);
src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Thu Sep 20 16:37:34 2007 +0200
+++ b/src/Pure/General/secure.ML	Thu Sep 20 17:48:16 2007 +0200
@@ -70,6 +70,6 @@
 (*override previous toplevel bindings!*)
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
-val use = Secure.use;
+fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
 val execute = Secure.execute;
 val system = Secure.system;