# HG changeset patch
# User berghofe
# Date 1333368567 -7200
# Node ID 8b63aaec0a0e5d4813bc7bb7676849880a6b45dd
# Parent  de84dd9a9dd4af43fd559d4e0302ab0a0cbedf9a# Parent  2511f3e8449628040b6e3bc41acb09765b001fd5
merged

diff -r 2511f3e84496 -r 8b63aaec0a0e src/HOL/SPARK/Tools/fdl_lexer.ML
--- 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