--- 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)