changeset 67522 | 9e712280cc37 |
parent 67446 | 1f4d167b6ac9 |
child 67569 | 5d71b114e7a3 |
--- a/src/Pure/PIDE/command.ML Sun Jan 28 16:09:00 2018 +0100 +++ b/src/Pure/PIDE/command.ML Sun Jan 28 19:28:52 2018 +0100 @@ -131,7 +131,7 @@ let val command_reports = Outer_Syntax.command_reports thy; - val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span)); + val proper_range = Token.range_of (drop_suffix Token.is_improper span); val pos = (case find_first Token.is_command span of SOME tok => Token.pos_of tok