# HG changeset patch
# User wenzelm
# Date 1361711511 -3600
# Node ID 3007d0bc9cb10af8172e6d5286dff847a13f625e
# Parent  1491459df1144aadcd1ce5b888f8bb913fc4e310
unified Command.is_proper in ML with Scala (see also 123be08eed88);

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