error diagnostics contain redundant file path info

[ciaran-matthew-dunne]

Diagnostics with "severity" 1 (i.e., errors) sent by the LSP contain redundant info about the file path:

This can be seen in the LSP logs:

      {
        "range": {
          "start": { "line": 7, "character": 0 },
          "end": { "line": 7, "character": 16 }
        },
        "severity": 4,
        "message": "nat"
      },
      {
        "range": {
          "start": { "line": 9, "character": 5 },
          "end": { "line": 9, "character": 12 }
        },
        "severity": 1,
        "message": "file:///home/ciaran/prog/eo2lp/lp/Syntax.lp:10:5-12 \nSet → Set\nis not unifiable with\nSet.\nfoo foo is not typable."
      },
      {
        "range": {
          "start": { "line": 12, "character": 7 },
          "end": { "line": 12, "character": 8 }
        },
        "severity": 4,
        "message": "OK"
      },
      {
        "range": {
          "start": { "line": 12, "character": 16 },
          "end": { "line": 12, "character": 16 }
        },
        "severity": 4,
        "message": "OK"
      },

This creates considerable visual clutter when using 'inline diagnostics':

Furthermore, I propose that the messages of diagnostics should avoid line breaks with \n.
Consider the diagnostic message:

"file:///home/ciaran/prog/eo2lp/lp/Syntax.lp:10:5-12 \nSet → Set\nis not unifiable with\nSet.\nfoo foo is not typable."

I guess that one motivation for the line-break-formatting here is to have some separation between lambdapi terms and English language. Instead, I propose that this message should contain no line breaks, and any lambdapi terms should be wrapped with 'backticks' like in Markdown. This way, the editors (VSCode, Emacs, Zed) can choose how to display these messages, possibly making use of syntax highlighting. For example, see the following diagnostic from the OCaml LSP displayed by the Ocaml plugin for the Zed editor: