diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-13 13:12:40 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-13 13:12:40 +0000 |
commit | 338608a73bc059670eb8196788c45a37419a3e4d (patch) | |
tree | 2938c4d34a758c94990dbd440f7ef722320f0dc2 /lib/pp.mli | |
parent | 098200d7e14805e8ae8b8f3873faec3ee3c096ad (diff) |
Made Pp.std_ppcmds opaque.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/pp.mli')
-rw-r--r-- | lib/pp.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 6316ab410..614023758 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -16,9 +16,7 @@ val make_pp_nonemacs:unit -> unit (** Pretty-printers. *) -type ppcmd - -type std_ppcmds = ppcmd Stream.t +type std_ppcmds (** {6 Formatting commands} *) @@ -36,13 +34,19 @@ val ismt : std_ppcmds -> bool val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref -(** {6 Concatenation. } *) +(** {6 Manipulation commands} *) -val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds +val app : std_ppcmds -> std_ppcmds -> std_ppcmds +(** Concatenation. *) -(** {6 Evaluation} *) +val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds +(** Infix alias for [app]. *) val eval_ppcmds : std_ppcmds -> std_ppcmds +(** Force computation. *) + +val is_empty : std_ppcmds -> bool +(** Test emptyness. *) (** {6 Derived commands} *) @@ -57,7 +61,7 @@ val qs : string -> std_ppcmds val quote : std_ppcmds -> std_ppcmds val strbrk : string -> std_ppcmds -val xmlescape : ppcmd -> ppcmd +val xmlescape : std_ppcmds -> std_ppcmds (** {6 Boxing commands} *) |