2021-11-18 20:09:09 +01:00
|
|
|
type glue =
|
|
|
|
|
{glen : float;
|
2021-11-20 00:21:37 +01:00
|
|
|
gstretch : float}
|
2021-11-18 20:09:09 +01:00
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
type element =
|
2021-11-20 00:21:37 +01:00
|
|
|
Text of string
|
2021-11-18 20:09:09 +01:00
|
|
|
| HGlue of glue
|
|
|
|
|
| VGlue of glue
|
|
|
|
|
| NewLine
|
|
|
|
|
| NewPage
|
2021-11-20 00:21:37 +01:00
|
|
|
| Font of (Pdftext.font * float)
|
2021-11-20 01:28:13 +01:00
|
|
|
| BeginDest of Pdfdest.t
|
|
|
|
|
| EndDest
|
2021-11-18 20:09:09 +01:00
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
type t = element list
|
2021-11-16 02:42:17 +01:00
|
|
|
|
2021-11-21 23:15:06 +01:00
|
|
|
val to_string : t -> string
|
|
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
val typeset : float -> float -> float -> float -> Pdfpaper.t -> Pdf.t -> t -> Pdfpage.t list
|
