# HG changeset patch
# User wenzelm
# Date 1400928909 -7200
# Node ID 0e5fa27d329319bb74fe5dbb0e7c56e0771247c8
# Parent  aa7f051ba6ab50586b1c14d86c9537f5b9bf0f03
strip trailing white space, to avoid notorious problems of jEdit with last line;

diff -r aa7f051ba6ab -r 0e5fa27d3293 src/Pure/Thy/thy_output.ML
--- 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;