merged
authorberghofe
Mon, 02 Apr 2012 14:09:27 +0200
changeset 47298 8b63aaec0a0e
parent 47297 de84dd9a9dd4 (diff)
parent 47270 2511f3e84496 (current diff)
child 47299 e705ef5ffe95
merged
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Apr 02 13:47:00 2012 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Apr 02 14:09:27 2012 +0200
@@ -174,6 +174,7 @@
   identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat);
 
 val whitespace = Scan.many (is_whitespace o symbol);
+val whitespace1 = Scan.many1 (is_whitespace o symbol);
 val whitespace' = Scan.many (is_whitespace' o symbol);
 val newline = Scan.one (is_newline o symbol);
 
@@ -261,7 +262,7 @@
   Scan.repeat (Scan.unless (Scan.one is_char_eof)
     (!!! "bad input"
        (   comment
-        || (keyword "For" -- whitespace) |--
+        || (keyword "For" -- whitespace1) |--
               Scan.repeat1 (Scan.unless (keyword ":") any) --|
               keyword ":" >> make_token Traceability
         || Scan.max leq_token