# HG changeset patch
# User wenzelm
# Date 1197651459 -3600
# Node ID 35e2aa8b8b0345b72ae053e6a8fb025ed665c666
# Parent  04b67ee7332746f40a5b3f4b78e43cc2f2c471f8
nested commands: avoid nested errors;

diff -r 04b67ee73327 -r 35e2aa8b8b03 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Dec 14 17:56:08 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 14 17:57:39 2007 +0100
@@ -754,7 +754,7 @@
       (case OuterSyntax.parse pos str of
         [transition] => Scan.succeed (K transition)
       | _ => Scan.fail_with (K "exactly one command expected"))
-      handle ERROR msg => Scan.fail_with (K ("malformed command\n" ^ msg))));
+      handle ERROR msg => Scan.fail_with (K msg)));
 
 
 
diff -r 04b67ee73327 -r 35e2aa8b8b03 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Dec 14 17:56:08 2007 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Dec 14 17:57:39 2007 +0100
@@ -113,7 +113,9 @@
       | get_pos (tok :: _) = T.pos_of tok;
 
     fun err (toks, NONE) = kind ^ get_pos toks
-      | err (toks, SOME msg) = kind ^ get_pos toks ^ ": " ^ msg;
+      | err (toks, SOME msg) =
+          if String.isPrefix kind msg then msg
+          else kind ^ get_pos toks ^ ": " ^ msg;
   in Scan.!! err scan end;
 
 fun !!! scan = cut "Outer syntax error" scan;