Handle multiline comments in Package (ipkg)

[stephen-smith]

Description

Alternative to #3384.

Implements multiline comments in ipkg to fulfill the promises of the existing documentation.

Should this change go in the CHANGELOG?

Added to _NEXT.

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[stephen-smith]

Is CONTRIBUTORS supposed to be maintained in alphabetical (or some other) order?

[CodingCellist]

Is CONTRIBUTORS supposed to be maintained in alphabetical (or some other) order?

It is meant to be in alphabetical order, yes (or at least, we try)

[mattpolzin]

I suppose this lacks a small amount of fidelity since the only useful meaning of the string within the comment would probably account for the fact that a block comment can start with a bracket followed by any number of dashes, but seeing as how 2 characters is the minimum at the start and end that doesn't feel too critical.

[stephen-smith]

Since we neither require a matching dash count on the end-of-comment token, nor strip excess leading dashes from eol comments, I don't feel this needs to change.

Parser/Lexer/Source.idr doesn't drop OR shrink for comments (of either type), but it also doesn't attempt to preserve their content in the tokens.