# HG changeset patch
# User wenzelm
# Date 1407789987 -7200
# Node ID ade8d65b212e8f0608c76d679cf542b966415d65
# Parent  3f1fd41ee8210fee9c495f7d286f9d4fd2202051
clarified Command_Span in accordance to Scala (see also c2c1e5944536);

diff -r 3f1fd41ee821 -r ade8d65b212e src/Pure/Thy/thy_syntax.ML
--- 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;