Florian Schanda <[email protected]> writes:
> On Friday 13 Dec 2013 16:36:04 Stephen Leake wrote:
>> In the meantime, specific examples are useful as test cases. In
>> particular, I'm curious as to how you prefer to indent them. So please
>> post some here; I'll add them to the tests, with "FIXME: failing -
>> aspects" comments.
>
> I guess I'll start with pre and postconditions. I suppose this would be a
> good
> way to indent them:
>
> procedure Foo (X : Integer;
> Y : out Integer)
> with Pre => X > 10 and
> X < 50 and
> F (X),
> Post =>
> Y >= X and
> Some_Very_Verbose_Predicate (X, Y);
I'm working on this; it required a grammar fix, and an indentation fix.
We currently indent a record type aspect as:
type Vector is tagged private
with
Constant_Indexing => Constant_Reference,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type;
'with' is indented by ada-indent-broken. That's not consistent with the
above subprogram aspect, so we should change that to:
type Vector is tagged private
with
Constant_Indexing => Constant_Reference,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type;
or indent the subprogram aspect.
> In words: align everything after the => to the column of the first non-
> whitespace character? Pre and postcondition expressions generally take this
> kind of form so that seems reasonable and readable to me. And here are some
> basic examples of SPARK 2014 aspects in their preferred form:
Where does this "preferred form" come from? I'd like to cite a
reference, if possible.
> While I remember, there will also be a new attribute in SPARK 2014 which
> looks
> like this (assume for example that X is a record type with fields A, B and C):
>
> Foo := X'Update (B => 12,
> C => Y);
this works fine in 5.1.2
--
-- Stephe
_______________________________________________
Emacs-ada-mode mailing list
[email protected]
http://host114.hostmonster.com/mailman/listinfo/emacs-ada-mode_stephe-leake.org
