message: Set source in diagnostics: goto erro shows multiline errors
  I'm not sure if this is a bug in vscode, but attaching a source to the error
  message changes the inline diagnostic message to show more than just the first
  line, see
  With this `F8` and `Shift-F8` show now a multi-line error.
diff: @@ -35,8 +35,10 @@ export class LeanDiagnosticsProvider implements Disposable {
  const range = new Range(pos, pos);
  let diagnostics = diagnosticMap.get(message.file_name);
  if (!diagnostics) diagnosticMap.set(message.file_name, diagnostics = []);
  - diagnostics.push(new Diagnostic(range, message.text,
  - toSeverity(message.severity)));
  + const d = new Diagnostic(range, message.text,
  + toSeverity(message.severity));
  + d.source = 'Lean';
  + diagnostics.push(d);
  }
  this.collection.clear();
  