changeset 58861 | 5ff61774df11 |
parent 58741 | 6e7b009e6d94 |
child 58864 | 505a8150368a |
--- a/src/Pure/Thy/thy_output.ML Sat Nov 01 14:20:38 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Nov 01 15:01:41 2014 +0100 @@ -413,7 +413,6 @@ make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); 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