message: Work around vscode hang on huge error messages.
diff: @@ -15,6 +15,27 @@ export interface ServerStatus {
  tasks: Task[];
  }
  +const MAX_MESSAGES = 2**13;
  +const MAX_MESSAGE_SIZE = 2**18;
  +function truncateMessages(msgs: Message[]): Message[] {
  + if (msgs.length >= MAX_MESSAGES) {
  + msgs = msgs.slice(0, MAX_MESSAGES - 1);
  + msgs.push({
  + ...msgs.pop(),
  + severity: 'error',
  + caption: undefined,
  + text: `Too many errors, only showing the first ${MAX_MESSAGES}.`,
  + });
  + }
  + msgs = msgs.map((msg) => ({
  + ...msg,
  + text: msg.text.length <= MAX_MESSAGE_SIZE ? msg.text :
  + msg.text.slice(0, MAX_MESSAGE_SIZE) +
  + `\n(message too long, truncated at ${MAX_MESSAGE_SIZE} characters)`,
  + }));
  + return msgs;
  +}
  +
  // A global channel for storing the contents of stderr.
  let stderrOutput: OutputChannel;
  @@ -91,6 +112,10 @@ export class Server extends leanclient.Server {
  }
  private attachEventHandlers() {
  + // HACK: limit number and size of messages, see
  + // https://leanprover-community.github.io/archive/113488general/25177foldingproblemsproblem.html
  + this.allMessages.on((res) => res.msgs = truncateMessages(res.msgs));
  +
  // When attaching event handlers ensure the global error log is clear.
  stderrOutput = stderrOutput || window.createOutputChannel('Lean: Server Errors');
  stderrOutput.clear();
  