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.
avoid handle_error (better msgs);
authorwenzelm
Thu, 07 Sep 2000 20:57:22 +0200
changeset 9901 09a142decdda
parent 9900 8035a13c61a0
child 9902 1ea354905d88
avoid handle_error (better msgs);
src/Pure/Isar/args.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle