diff options
Diffstat (limited to 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 2 |
1 files changed, 2 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) >] |