Dot leaders finished

This commit is contained in:
John Whitington 2024-12-03 18:17:12 +00:00
parent 7145a558eb
commit 5f1446b59b

View File

@ -94,17 +94,13 @@ let used pdf fastrefnums labels title marks =
marks; marks;
codepoints 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 make_dots space fontpack fontsize =
let dots_width, dots = let dotruns = of_utf8 fontpack fontsize "." in
let dotruns = of_utf8 fontpack fontsize "." in let dotwidth = width_of_runs dotruns in
let dotwidth = width_of_runs dotruns in let runs = flatten (many dotruns (int_of_float (floor (space /. dotwidth)))) in
let runs = flatten (many dotruns (int_of_float (floor (space /. dotwidth)))) in let remainder = space -. width_of_runs runs in
(width_of_runs runs, runs) [Cpdftype.HGlue remainder] @ 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]
(* Typeset a table of contents with given font, font size and title. Mediabox (* 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 (and CropBox) copied from first page of existing PDF. Margin of 10% inside