# HG changeset patch # User berghofe # Date 1351854051 -3600 # Node ID ad8a6db0b480b42151456dcbd43e88a60939d85b # Parent dbbf9578e7127fdf8ca0b7e395dbe2ad27028c7e Allow parentheses around left-hand sides of array associations diff -r dbbf9578e712 -r ad8a6db0b480 src/HOL/SPARK/Tools/fdl_parser.ML --- a/src/HOL/SPARK/Tools/fdl_parser.ML Thu Nov 01 15:00:48 2012 +0100 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML Fri Nov 02 12:00:51 2012 +0100 @@ -166,6 +166,8 @@ val quantification_generator = list1 identifier --| $$$ ":" -- identifier; +fun opt_parens p = $$$ "(" |-- p --| $$$ ")" || p; + fun expression xs = group "expression" (binop disjunction ($$$ "->" || $$$ "<->")) xs @@ -214,14 +216,14 @@ (list1 (identifier --| $$$ ":=" -- !!! expression) >> (pair s #> Record)) xs and array_args s xs = - ( expression -- Scan.optional ($$$ "," |-- !!! array_associations) [] >> - (fn (default, assocs) => Array (s, SOME default, assocs)) - || array_associations >> (fn assocs => Array (s, NONE, assocs))) xs + ( array_associations >> (fn assocs => Array (s, NONE, assocs)) + || expression -- Scan.optional ($$$ "," |-- !!! array_associations) [] >> + (fn (default, assocs) => Array (s, SOME default, assocs))) xs and array_associations xs = - (list1 (enum1 "&" ($$$ "[" |-- + (list1 (opt_parens (enum1 "&" ($$$ "[" |-- !!! (list1 (expression -- Scan.option ($$$ ".." |-- !!! expression)) --| - $$$ "]")) --| $$$ ":=" -- expression)) xs; + $$$ "]"))) --| $$$ ":=" -- expression)) xs; (* verification conditions *)