diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml4 | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index bfabb533ba..415a3002ab 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -140,6 +140,8 @@ let strbrk s = else if p=n then [< >] else [< str (String.sub s p (n-p)) >] in aux 0 0 +let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false + (* boxing commands *) let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >] let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >] diff --git a/lib/pp.mli b/lib/pp.mli index 8a5aee7993..41ea9ca0f0 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -35,6 +35,7 @@ val fnl : unit -> std_ppcmds val pifb : unit -> std_ppcmds val ws : int -> std_ppcmds val mt : unit -> std_ppcmds +val ismt : std_ppcmds -> bool val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref |