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.
No longer treat "title" as FDL keyword
authorberghofe
Thu, 22 Mar 2012 10:10:02 +0100
changeset 47083 d04b38d4035b
parent 47077 3031603233e3
child 47084 2e3dcec91653
No longer treat "title" as FDL keyword
src/HOL/SPARK/Tools/fdl_lexer.ML file | annotate | diff | comparison | revisions
src/HOL/SPARK/Tools/fdl_parser.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Mar 21 23:41:22 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Mar 22 10:10:02 2012 +0100
@@ -96,7 +96,6 @@
 
 val lexicon = Scan.make_lexicon (map raw_explode
   ["rule_family",
-   "title",
    "For",
    ":",
    "[",
--- a/src/HOL/SPARK/Tools/fdl_parser.ML	Wed Mar 21 23:41:22 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Mar 22 10:10:02 2012 +0100
@@ -323,7 +323,7 @@
    $$$ ":" -- identifier)) >> add_fun_decl) x;
 
 fun declarations x =
- ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+ (the_identifier "title" |-- subprogram_kind -- identifier --| $$$ ";" --
   (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
      !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
   $$$ "end" --| $$$ ";") x;
isabelle