| changeset 51266 | 3007d0bc9cb1 |
| parent 50914 | fe4714886d92 |
| child 51284 | 59a03019f3bf |
--- a/src/Pure/PIDE/command.ML Sun Feb 24 13:46:14 2013 +1100 +++ b/src/Pure/PIDE/command.ML Sun Feb 24 14:11:51 2013 +0100 @@ -23,7 +23,7 @@ (* span range *) val range = Token.position_range_of; -val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space; +val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper; (* memo results *)