feat: F4.8d the documentation mode's report as a PDF, as Java's

ReportRun reads Java's report back with iText: every piece of text with its place, font, size and colour. The editor lays the report out by iText's rules (A4, leading 1.5, loose chunks in the current line, tables 80 % wide with padding 2, fixed traffic columns, page breaks) and draws it with pdf-lib in the PDF's own Helvetica, widths without kerning as iText measures. All device pages of Internet_Komplett, the first page and the data exchange of einfaches_rechnernetz_komplett match Java piece by piece; Java's iText reads our PDF with the same text in the same places. The sidebar gains Java's "Report"; the frames come from the room by a short subscription. Not adopted: true/false for DHCP (Java's own Ja/Nein), hash table orders, an image running off the page, the report writing back into the model. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-04 12:35:35 +00:00
parent 7e68414bb2
commit b8b999fd66
29 changed files with 7726 additions and 23 deletions
@@ -0,0 +1,262 @@
+// The page layout of FILIUS' report, as iText 5 lays out what Java's
+// ReportGenerator adds to its Document (measured with tools/java-oracle's
+// ReportRun): A4 with 36 to spare around; a paragraph's lines 1.5 times its
+// largest font apart, and loose text (a chunk added to the document) in the
+// current line, at the last paragraph's spacing, until a new line ends it;
+// lines broken after a space or a hyphen, a word wider than the line where
+// it reaches the edge; a line that would end below the margin begins the
+// next page. A table is 80 % of the width (or as wide as its columns when
+// they are fixed), its columns in proportion, each cell's text 2 inside it,
+// its lines as far apart as its font is large; a row that would end below
+// the margin begins the next page. An image is as wide as the page, half a
+// line below the last one. What is laid out is a list of pages of things to
+// draw, in PDF coordinates (from the bottom up).
+//
+// Better than Java: an image taller than the rest of the page begins the
+// next one, and one taller than a page is made smaller to fit (iText draws
+// it beyond the page's edge).
+
+export type ReportFont = 'Helvetica' | 'Helvetica-Bold';
+export type Rgb = readonly [number, number, number];
+
+export interface TextStyle {
+  readonly font: ReportFont;
+  readonly size: number;
+  readonly color: Rgb;
+}
+
+export type ReportOp =
+  | { readonly kind: 'text'; readonly text: string; readonly x: number; readonly y: number; readonly font: ReportFont; readonly size: number; readonly color: Rgb }
+  | { readonly kind: 'rect'; readonly x: number; readonly y: number; readonly width: number; readonly height: number; readonly color: Rgb }
+  | { readonly kind: 'image'; readonly x: number; readonly y: number; readonly width: number; readonly height: number };
+
+/** How wide a text is in a font (without kerning, as iText measures), and the text as the font can write it. */
+export interface ReportFonts {
+  readonly width: (text: string, font: ReportFont, size: number) => number;
+  readonly clean: (text: string) => string;
+}
+
+export interface TableCell {
+  readonly text: string;
+  readonly style: TextStyle;
+  readonly background?: Rgb;
+}
+
+export interface TableSpec {
+  /** The columns' widths: in proportion, or fixed when `fixed`. */
+  readonly widths: readonly number[];
+  readonly fixed?: boolean;
+  readonly align: 'left' | 'center';
+  readonly rows: readonly (readonly TableCell[])[];
+}
+
+/** PageSize.A4 and Document's margins. */
+export const PAGE_WIDTH = 595;
+export const PAGE_HEIGHT = 842;
+export const MARGIN = 36;
+const TOP = PAGE_HEIGHT - MARGIN;
+const BOTTOM = MARGIN;
+const LEFT = MARGIN;
+const WIDTH = PAGE_WIDTH - 2 * MARGIN;
+/** PdfPTable's width without a fixed one: 80 % of the page's. */
+const TABLE_SHARE = 0.8;
+/** PdfPCell's padding. */
+const PADDING = 2;
+
+/** Words in a style, as a paragraph or a chunk takes them. */
+export interface Words {
+  readonly text: string;
+  readonly style: TextStyle;
+}
+
+interface Piece extends Words {
+  /** The chunk it is of: a line draws each chunk's part as one text, as iText does. */
+  readonly chunk: number;
+}
+
+/** A text's pieces to break a line after: up to and with each space or hyphen. */
+const breakable = (text: string) => text.match(/[^ -]*[ -]|[^ -]+/g) ?? [];
+
+export class ReportWriter {
+  private readonly pages: ReportOp[][] = [[]];
+  private y = TOP;
+  /** The spacing of loose text: the last paragraph's. */
+  private leading = 0;
+  private pending: Piece[] = [];
+
+  constructor(private readonly fonts: ReportFonts) {}
+
+  private get page(): ReportOp[] {
+    return this.pages[this.pages.length - 1]!;
+  }
+
+  private newPage(): void {
+    this.pages.push([]);
+    this.y = TOP;
+  }
+
+  private width(piece: Words): number {
+    return this.fonts.width(piece.text, piece.style.font, piece.style.size);
+  }
+
+  /** Pieces broken into lines of a width. */
+  private lines(pieces: readonly Piece[], width: number): Piece[][] {
+    const lines: Piece[][] = [];
+    let line: Piece[] = [];
+    let used = 0;
+    const push = () => {
+      lines.push(line);
+      line = [];
+      used = 0;
+    };
+    for (const piece of pieces) {
+      for (const part of breakable(piece.text)) {
+        const word = { text: part, style: piece.style, chunk: piece.chunk };
+        const fits = used + this.width({ ...word, text: part.trimEnd() }) <= width;
+        if (fits) {
+          line.push(word);
+          used += this.width(word);
+          continue;
+        }
+        if (line.length > 0) push();
+        // On a line of its own, broken where it reaches the edge (a word that fits is not).
+        for (const character of part) {
+          const one = { text: character, style: piece.style, chunk: piece.chunk };
+          if (line.length > 0 && used + this.width({ ...one, text: character.trimEnd() }) > width) push();
+          line.push(one);
+          used += this.width(one);
+        }
+      }
+    }
+    if (line.length > 0 || lines.length === 0) push();
+    return lines;
+  }
+
+  /** A line's pieces as texts to draw: one per run of a style, without the spaces at its end. */
+  private runs(line: readonly Piece[]): Piece[] {
+    const runs: Piece[] = [];
+    for (const piece of line) {
+      const last = runs[runs.length - 1];
+      if (last !== undefined && last.chunk === piece.chunk) runs[runs.length - 1] = { text: last.text + piece.text, style: last.style, chunk: last.chunk };
+      else runs.push(piece);
+    }
+    while (runs.length > 0) {
+      const last = runs[runs.length - 1]!;
+      const text = last.text.trimEnd();
+      if (text !== '') {
+        runs[runs.length - 1] = { text, style: last.style, chunk: last.chunk };
+        break;
+      }
+      runs.pop();
+    }
+    return runs;
+  }
+
+  /** Writes lines at a spacing, each a line below the last, on the next page where it would end below the margin. */
+  private writeLines(lines: readonly Piece[][], leading: number, align: 'left' | 'center'): void {
+    for (const line of lines) {
+      if (this.y - leading < BOTTOM) this.newPage();
+      this.y -= leading;
+      const runs = this.runs(line);
+      const used = runs.reduce((sum, run) => sum + this.width(run), 0);
+      let x = align === 'center' ? LEFT + (WIDTH - used) / 2 : LEFT;
+      for (const run of runs) {
+        this.page.push({ kind: 'text', text: run.text, x, y: this.y, font: run.style.font, size: run.style.size, color: run.style.color });
+        x += this.width(run);
+      }
+    }
+  }
+
+  /** Ends the current line of loose text, if there is one. */
+  private endPending(evenEmpty: boolean): void {
+    if (this.pending.length === 0 && !evenEmpty) return;
+    this.writeLines(this.lines(this.pending, WIDTH), this.leading, 'left');
+    this.pending = [];
+  }
+
+  private chunks = 0;
+
+  /** The pieces as the fonts write them, each its own chunk. */
+  private clean(pieces: readonly Words[]): Piece[] {
+    return pieces.map((piece) => ({ text: this.fonts.clean(piece.text), style: piece.style, chunk: this.chunks++ }));
+  }
+
+  /** A paragraph (Paragraph): its own lines, 1.5 times its largest font apart; that spacing goes on for loose text. */
+  paragraph(pieces: readonly Words[], align: 'left' | 'center' = 'left'): void {
+    this.endPending(false);
+    this.leading = 1.5 * Math.max(...pieces.map((piece) => piece.style.size));
+    this.writeLines(this.lines(this.clean(pieces), WIDTH), this.leading, align);
+  }
+
+  /** Loose text (a Chunk added to the document): in the current line. */
+  chunk(text: string, style: TextStyle): void {
+    this.pending.push(...this.clean([{ text, style }]));
+  }
+
+  /** A new line (Chunk.NEWLINE): ends the current line, an empty one too. */
+  newline(): void {
+    this.endPending(true);
+  }
+
+  /** A table (PdfPTable), row by row; a row that would end below the margin begins the next page. */
+  table(spec: TableSpec): void {
+    this.endPending(false);
+    const total = spec.fixed === true ? spec.widths.reduce((sum, each) => sum + each, 0) : WIDTH * TABLE_SHARE;
+    const sum = spec.widths.reduce((all, each) => all + each, 0);
+    const widths = spec.widths.map((each) => (spec.fixed === true ? each : (each / sum) * total));
+    const left = spec.align === 'center' ? LEFT + (WIDTH - total) / 2 : LEFT;
+    for (const row of spec.rows) {
+      const cells = row.map((cell, index) => {
+        const lines = cell.text.split('\n').flatMap((part) => this.lines(this.clean([{ text: part, style: cell.style }]), widths[index]! - 2 * PADDING));
+        return { cell, lines };
+      });
+      // A cell's lines as far apart as its font is large.
+      const height = 2 * PADDING + Math.max(...cells.map(({ cell, lines }) => lines.length * cell.style.size));
+      if (this.y - height < BOTTOM) this.newPage();
+      let x = left;
+      cells.forEach(({ cell, lines }, index) => {
+        if (cell.background !== undefined) this.page.push({ kind: 'rect', x, y: this.y - height, width: widths[index]!, height, color: cell.background });
+        lines.forEach((line, number) => {
+          const y = this.y - PADDING - (number + 1) * cell.style.size;
+          let at = x + PADDING;
+          for (const run of this.runs(line)) {
+            this.page.push({ kind: 'text', text: run.text, x: at, y, font: run.style.font, size: run.style.size, color: run.style.color });
+            at += this.width(run);
+          }
+        });
+        x += widths[index]!;
+      });
+      this.y -= height;
+    }
+  }
+
+  /** An image (Image scaled to the page's width), half a line below the last line. */
+  image(pixels: { readonly width: number; readonly height: number }): void {
+    this.endPending(false);
+    let width = WIDTH;
+    let height = (WIDTH * pixels.height) / pixels.width;
+    let top = this.y - this.leading / 2;
+    if (top - height < BOTTOM && this.page.length > 0) {
+      this.newPage();
+      top = this.y - this.leading / 2;
+    }
+    if (top - height < BOTTOM) {
+      height = top - BOTTOM;
+      width = (height * pixels.width) / pixels.height;
+    }
+    this.page.push({ kind: 'image', x: LEFT, y: top - height, width, height });
+    this.y = top - height;
+  }
+
+  /** A new page (Chunk.NEXTPAGE). */
+  nextPage(): void {
+    this.endPending(false);
+    this.newPage();
+  }
+
+  /** The pages, the last one without an empty end. */
+  finish(): ReportOp[][] {
+    this.endPending(false);
+    return this.page.length === 0 && this.pages.length > 1 ? this.pages.slice(0, -1) : [...this.pages];
+  }
+}