From 5f1446b59b4fa0ef050a74f65f38f703cbe3056c Mon Sep 17 00:00:00 2001 From: John Whitington Date: Tue, 3 Dec 2024 18:17:12 +0000 Subject: [PATCH] Dot leaders finished --- cpdftoc.ml | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/cpdftoc.ml b/cpdftoc.ml index 0c2ed3d..5d8301c 100644 --- a/cpdftoc.ml +++ b/cpdftoc.ml @@ -94,17 +94,13 @@ let used pdf fastrefnums labels title marks = marks; codepoints -(* Fill the space with a small space, maybe some dots, then maybe a final tiny space *) +(* Make a dot leader *) let make_dots space fontpack fontsize = - let dots_width, dots = - let dotruns = of_utf8 fontpack fontsize "." in - let dotwidth = width_of_runs dotruns in - let runs = flatten (many dotruns (int_of_float (floor (space /. dotwidth)))) in - (width_of_runs runs, runs) - in - let right_space = space -. dots_width in - let left_space = space -. dots_width -. right_space in - [Cpdftype.HGlue left_space] @ dots @ [Cpdftype.HGlue right_space] + let dotruns = of_utf8 fontpack fontsize "." in + let dotwidth = width_of_runs dotruns in + let runs = flatten (many dotruns (int_of_float (floor (space /. dotwidth)))) in + let remainder = space -. width_of_runs runs in + [Cpdftype.HGlue remainder] @ runs (* Typeset a table of contents with given font, font size and title. Mediabox (and CropBox) copied from first page of existing PDF. Margin of 10% inside