tuned fail;
authorwenzelm
Sat, 04 Apr 1998 14:27:11 +0200
changeset 4797 d66477d29598
parent 4796 e70ae8578792
child 4798 7cfc85fc6fd7
tuned fail;
src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Sat Apr 04 12:31:35 1998 +0200
+++ b/src/Pure/attribute.ML	Sat Apr 04 14:27:11 1998 +0200
@@ -55,7 +55,7 @@
 fun fail name msg = raise FAIL (name, msg);
 
 fun warn_failed (name, msg) =
-  warning ("Invocation of " ^ quote name ^ " attribute failed: " ^ msg);
+  warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
 
 fun apply (x, []) = x
   | apply (x, f :: fs) = apply (f x handle FAIL info => (warn_failed info; x), fs);
@@ -140,7 +140,7 @@
     val name = NameSpace.intern space raw_name;
   in
     (case Symtab.lookup (attrs, name) of
-      None => error ("Unknown attribute: " ^ quote name)
+      None => raise FAIL (name, "unknown attribute")
     | Some p => which p args)
   end;