Overhaul side-information in textual notation

[MattWindsor91]

The textual notation is a bit inconsistent as to how to encode modalities, inflections, and side information. Usually this is done by separating the main material from the side material using a :, but this falls apart with things like loop headers (which are not always separated), message sets and assertions (which use : for something else), target instantiations, and so on.

This issue proposes that:

• : is used for introducing definitions (so assertion A: Blah holds and message set A: universe are still ok);
• parentheses are used for introducing side information (so, loop LoopName (forever), alternative (hot), and maybe (sequence group A (module M -> world)).

The idea here is that the syntax should really follow normal English conventions, where we might expect a term and its definition to be separated by ':' and side information to be given in parentheses.

This is part of a general concern I have with respect to making sure that the textual notation is understandable and self-consistent.

[MattWindsor91]

Also, reminder to myself to check what MSC does here. I know it has a textual notation but haven't dug deep into it.

[MattWindsor91]

This change would eliminate the weird rule about being able to specify loop forever, loop: forever, and loop L: forever, but not loop L forever.