message: chore: rm dead code & document & ensure update
diff: @@ -171,35 +171,7 @@ export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}
  return <LspDiagnosticsContext.Provider value={allDiags}>{children}</LspDiagnosticsContext.Provider>
  }
  +/** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */
  export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic {
  return { ...(diag as LeanDiagnostic), message: { text: diag.message } };
  }
  -
  -export function useMessagesForFile(rs: RpcSessionAtPos, uri: DocumentUri, line?: number): InteractiveDiagnostic[] {
  - const sv = React.useContext(VersionContext)
  - const lspDiags = React.useContext(LspDiagnosticsContext)
  - const [diags, setDiags] = React.useState<InteractiveDiagnostic[]>([])
  -
  - async function updateDiags() {
  - setDiags((lspDiags.get(uri) || []).map(lspDiagToInteractive));
  - if (sv?.hasWidgetsV1()) {
  - try {
  - const diags = await getInteractiveDiagnostics(rs,
  - line ? { start: line, end: line + 1 } : undefined)
  - if (diags.length > 0) {
  - // diags may be [] when lake fails
  - setDiags(diags)
  - }
  - } catch (err: any) {
  - if (err?.code === -32801) {
  - // Document has been changed since we made the request.
  - // This can happen while typing quickly, so server will catch up on next edit.
  - } else {
  - console.log('getInteractiveDiagnostics error ', err)
  - }
  - }
  - }
  - }
  - React.useEffect(() => { void updateDiags() }, [uri, line, rs, lspDiags.get(uri)])
  - return diags;
  -}
  