diff -r 1491459df114 -r 3007d0bc9cb1 src/Pure/PIDE/command.ML
--- 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 *)