* Builds the output PDF filename: strips any directory components and * normalizes to a single `.pdf` extension.
(fileName: string | undefined)
| 136 | * normalizes to a single `.pdf` extension. |
| 137 | */ |
| 138 | function buildPdfFileName(fileName: string | undefined): string { |
| 139 | const base = (fileName || 'document').split(/[/\\]/).pop()?.trim() || 'document' |
| 140 | const withoutExtension = base.toLowerCase().endsWith('.pdf') ? base.slice(0, -4) : base |
| 141 | return `${withoutExtension || 'document'}.pdf` |
| 142 | } |
| 143 | |
| 144 | /** |
| 145 | * Extracts TeX error lines (lines starting with `!`, each with two lines of |