changeset 74174 | a3b0fc510705 |
parent 74171 | a9e79c3645c4 |
child 74175 | 53e28c438f96 |
--- a/src/Pure/Isar/token.ML Mon Aug 23 13:23:48 2021 +0200 +++ b/src/Pure/Isar/token.ML Mon Aug 23 14:24:57 2021 +0200 @@ -381,7 +381,7 @@ fun file_source (file: file) = let val text = cat_lines (#lines file); - val end_pos = Position.advance_symbol_explode text (#pos file); + val end_pos = Position.symbol_explode text (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files