diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 35 |
1 files changed, 17 insertions, 18 deletions
@@ -1,30 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp_control -(*i*) -(* Modify pretty printing functions behavior for emacs ouput (special +(** Modify pretty printing functions behavior for emacs ouput (special chars inserted at some places). This function should called once in module [Options], that's all. *) val make_pp_emacs:unit -> unit val make_pp_nonemacs:unit -> unit -(* Pretty-printers. *) +(** Pretty-printers. *) type ppcmd type std_ppcmds = ppcmd Stream.t -(*s Formatting commands. *) +(** {6 Formatting commands. } *) val str : string -> std_ppcmds val stras : int * string -> std_ppcmds @@ -40,11 +36,11 @@ val ismt : std_ppcmds -> bool val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref -(*s Concatenation. *) +(** {6 Concatenation. } *) val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds -(*s Derived commands. *) +(** {6 Derived commands. } *) val spc : unit -> std_ppcmds val cut : unit -> std_ppcmds @@ -59,7 +55,7 @@ val strbrk : string -> std_ppcmds val xmlescape : ppcmd -> ppcmd -(*s Boxing commands. *) +(** {6 Boxing commands. } *) val h : int -> std_ppcmds -> std_ppcmds val v : int -> std_ppcmds -> std_ppcmds @@ -67,7 +63,7 @@ val hv : int -> std_ppcmds -> std_ppcmds val hov : int -> std_ppcmds -> std_ppcmds val t : std_ppcmds -> std_ppcmds -(*s Opening and closing of boxes. *) +(** {6 Opening and closing of boxes. } *) val hb : int -> std_ppcmds val vb : int -> std_ppcmds @@ -77,7 +73,7 @@ val tb : unit -> std_ppcmds val close : unit -> std_ppcmds val tclose : unit -> std_ppcmds -(*s Pretty-printing functions \emph{without flush}. *) +(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *) val pp_with : Format.formatter -> std_ppcmds -> unit val ppnl_with : Format.formatter -> std_ppcmds -> unit @@ -87,31 +83,34 @@ val pp_flush_with : Format.formatter -> unit -> unit val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit -(*s Pretty-printing functions \emph{with flush}. *) +(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *) val msg_with : Format.formatter -> std_ppcmds -> unit val msgnl_with : Format.formatter -> std_ppcmds -> unit -(*s The following functions are instances of the previous ones on +(** {6 ... } *) +(** The following functions are instances of the previous ones on [std_ft] and [err_ft]. *) -(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *) +(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *) val pp : std_ppcmds -> unit val ppnl : std_ppcmds -> unit val pperr : std_ppcmds -> unit val pperrnl : std_ppcmds -> unit -val message : string -> unit (* = pPNL *) +val message : string -> unit (** = pPNL *) val warning : string -> unit val warn : std_ppcmds -> unit val pp_flush : unit -> unit val flush_all: unit -> unit -(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *) +(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *) val msg : std_ppcmds -> unit val msgnl : std_ppcmds -> unit val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit + +val string_of_ppcmds : std_ppcmds -> string |