diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -168,7 +168,7 @@
   {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
-      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
         map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)