Add syntax for Judoc blocks

[janmasrovira]

• Closes Support block judoc comments #2050

This pr adds the possibility to give judoc documentation in blocks delimited by {-- and --}.

• Inside these blocks, normal comments are disabled.
• It is allowed to have multiple blocks associated with the same identifier, e.g.

{-- an axiom --}
{-- of type ;Type; --}
axiom a : Type;

• Nested blocks are not allowed.
• Blocks can be empty: {-- --}.
• The formatter respects line breaks inside blocks.
• The formatter normalizes whitespace at both ends of the block to a single whitespace.