- tags(+Lines:lines, -Tags, -RestLines) is semidet[private]
- If the first line is a @tag, read the leading run of @tag lines
into Tags and return the remaining lines (e.g., a section header
ending the tag block) as RestLines. Fails if no tag is collected,
so the caller falls through to normal block parsing.