# HG changeset patch
# User berghofe
# Date 1333367939 -7200
# Node ID de84dd9a9dd4af43fd559d4e0302ab0a0cbedf9a
# Parent  29aa0c0718752f0faa264cb4a0679258022c04d0
Require "For" keyword to be followed by at least one whitespace, to avoid that
identifiers starting with "For" are interpreted as traceability information

diff -r 29aa0c071875 -r de84dd9a9dd4 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Apr 02 10:49:03 2012 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Apr 02 13:58:59 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