diff options
Diffstat (limited to 'src/util.mli')
| -rw-r--r-- | src/util.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/util.mli b/src/util.mli index 73dbd30b..39bc8a19 100644 --- a/src/util.mli +++ b/src/util.mli @@ -228,3 +228,15 @@ val is_some : 'a option -> bool val is_none : 'a option -> bool val take : int -> 'a list -> 'a list + +val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list) + +(* Terminal color codes *) +val termcode : int -> string +val bold : string -> string +val green : string -> string +val red : string -> string +val yellow : string -> string +val cyan : string -> string +val blue : string -> string +val clear : string -> string |