unified Command.is_proper in ML with Scala (see also 123be08eed88);

--- a/src/Pure/Isar/token.ML	Sun Feb 24 13:46:14 2013 +1100
+++ b/src/Pure/Isar/token.ML	Sun Feb 24 14:11:51 2013 +0100
@@ -32,6 +32,7 @@
   val is_command: T -> bool
   val is_name: T -> bool
   val is_proper: T -> bool
+  val is_improper: T -> bool
   val is_semicolon: T -> bool
   val is_comment: T -> bool
   val is_begin_ignore: T -> bool
@@ -172,6 +173,8 @@
   | is_proper (Token (_, (Comment, _), _)) = false
   | is_proper _ = true;
 
+val is_improper = not o is_proper;
+
 fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
   | is_semicolon _ = false;
 

--- 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 *)