diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Pure/ML/ml_lex.scala	Fri Aug 05 16:30:53 2016 +0200
@@ -66,6 +66,8 @@
   {
     def is_keyword: Boolean = kind == Kind.KEYWORD
     def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
+    def is_space: Boolean = kind == Kind.SPACE
+    def is_comment: Boolean = kind == Kind.COMMENT
   }