clarified Command_Span in accordance to Scala (see also c2c1e5944536);

--- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:43:26 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:46:27 2014 +0200
@@ -85,8 +85,8 @@
 fun ship span =
   let
     val kind =
-      if not (null span) andalso Token.is_command (hd span) then
-        Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
+      if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
+      then Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
       else if forall Token.is_improper span then Ignored_Span
       else Malformed_Span;
   in cons (Span (kind, span)) end;