Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Require "For" keyword to be followed by at least one whitespace, to avoid that
authorberghofe
Mon, 02 Apr 2012 13:58:59 +0200
changeset 47297 de84dd9a9dd4
parent 47269 29aa0c071875
child 47298 8b63aaec0a0e
Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information
src/HOL/SPARK/Tools/fdl_lexer.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle