JSON problem matchers should support `"loop": true` in patterns other than the last one

[JasonGross]

Describe the enhancement
According to https://github.com/actions/toolkit/blob/master/docs/problem-matchers.md#single-line-matchers:

loop: whether to loop until a match is not found, only valid on the last pattern of a multipattern matcher

However, I would like to be able to loop in the middle of a pattern, and then, once there are no more matches for that pattern, accumulate a couple more lines.

Code Snippet

In particular, the pattern I want to use is:

{
    "problemMatcher": [
        {
            "owner": "coq-problem-matcher-multiline",
            "pattern": [
                {
                    "regexp": "^File \"([^ \"]+)\", line (\\d+), characters (\\d+-\\d+):",
                    "file": 1,
                    "line": 2,
                    "column": 3
                },
                {
                    "regexp": "^(Warning|Error):\\s*((?:[^\\]]|\\].)*)$",
                    "severity": 1,
                    "message": 2
                },
                {
                    "regexp": "^((?:[^\\]]|\\].)*)$",
                    "severity": 1,
                    "message": 2,
                    "loop": true
                },
                {
                    "regexp": "^(.*?)\\s*\\[(.*)\\]$",
                    "message": 1,
                    "code": 2
                }
            ]
        }
    ]
}

That is, an error message starts with a line File "<FILE>", line <LINE>, characters <COLUMN>:, followed by a line starting with either Warning: or Error:, followed by a potentially multiline message which is recognized as ending with [<CODE>] followed by a newline. (The matcher I wrote isn't perfect, and I end up needing four separate matchers: one for one-line messages, one for two-line messages (unless "loop": true allows zero-or-more rather than one-or-more?), and one for three-or-more-line messages.)

Additional information

Trying this out in mit-plv/fiat-crypto#910