# HG changeset patch
# User wenzelm
# Date 968353042 -7200
# Node ID 09a142decdda57348c87774bef4100717e2a1441
# Parent  8035a13c61a0f717baeb5672c940a082771e10b7
avoid handle_error (better msgs);

diff -r 8035a13c61a0 -r 09a142decdda src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Sep 07 20:56:58 2000 +0200
+++ b/src/Pure/Isar/args.ML	Thu Sep 07 20:57:22 2000 +0200
@@ -64,7 +64,7 @@
 fun val_of (Arg (_, (x, _))) = x;
 fun pos_of (Arg (_, (_, pos))) = pos;
 
-fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
+fun str_of (Arg (Ident, (x, _))) = x
   | str_of (Arg (String, (x, _))) = quote x
   | str_of (Arg (Keyword, (x, _))) = x
   | str_of (Arg (EOF, _)) = "end-of-text";
@@ -214,10 +214,9 @@
 (* argument syntax *)
 
 fun syntax kind scan (src as Src ((s, args), pos)) st =
-  (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
-    OK (Some x, (st', [])) => (st', x)
-  | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
-  | Error msg => err_in_src kind ("\n" ^ msg) src);
+  (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
+    (Some x, (st', [])) => (st', x)
+  | (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos)));
 
 
 (* attribs *)