--- a/src/Pure/Thy/thy_output.ML Fri May 23 14:25:14 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat May 24 12:55:09 2014 +0200
@@ -412,8 +412,10 @@
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
- val spans =
- Source.of_list (filter_out Token.is_semicolon toks)
+ val spans = toks
+ |> filter_out Token.is_semicolon
+ |> take_suffix Token.is_space |> #1
+ |> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
|> Source.source stopper (Scan.error (Scan.bulk span)) NONE
|> Source.exhaust;