#332 Refines clause on INITIALISATION event ignored

[Fabian]

As discussed in bug #2810797 the RodinDB doesn't save the name of an extended event for INITIALISATION events because it would be redundant information. Anyhow it is possible for a plug-in to set a refines clause for an INITIALISATION event which is extended. The RodinDB doesn't report an error/warning here.

How to reproduce:
Execute the following lines for an INITIALISATION event:
IRefinesEvent refinesEvent = rodinEvent.getRefinesClause(getNewName());
refinesEvent.create(null, monitor);
refinesEvent.setAbstractEventLabel("some_name", monitor);

Expected behaviour:
Error or warning marker on resource

Seen behaviour:
No problem reported

[Laurent Voisin]

This is correctly reported by the static checker as a warning marker: "Initialisation must not refine explicitly".

Note: you need to save the machine and have the builder enable for the static checker to run.

[Fabian]

Ah, sorry, my mistake... ;-)

Maybe the error message could be improved for the case when 'extends' is set.

[Laurent Voisin]

'extends' doesn't change anything. The refinement is still there. Extension is just a decoration of the refinement relation.

No need to change the message.