diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0abb47c22..7fc3279af 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -12,6 +12,12 @@ open Miniml open Mlutil open Pp +(** By default, in module Format, you can do horizontal placing of blocks + even if they include newlines, as long as the number of chars in the + blocks are less that a line length. To avoid this awkward situation, + we attach a big virtual size to [fnl] newlines. *) + +val fnl : unit -> std_ppcmds val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds |