diff options
Diffstat (limited to 'tools/coqdoc/output.mli')
-rw-r--r-- | tools/coqdoc/output.mli | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli new file mode 100644 index 00000000..2195fa53 --- /dev/null +++ b/tools/coqdoc/output.mli @@ -0,0 +1,92 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) + +open Index + +type target_language = LaTeX | HTML | TeXmacs + +val target_language : target_language ref + +val set_out_file : string -> unit +val output_dir : string ref +val close : unit -> unit + +val quiet : bool ref +val short : bool ref +val light : bool ref +val header_trailer : bool ref +val index : bool ref +val multi_index : bool ref +val toc : bool ref +val title : string ref +val externals : bool ref +val coqlib : string ref +val raw_comments : bool ref + +val charset : string ref +val inputenc : string ref +val set_latin1 : unit -> unit +val set_utf8 : unit -> unit + +val add_printing_token : string -> string option * string option -> unit +val remove_printing_token : string -> unit + +val set_module : coq_module -> unit + +val header : unit -> unit +val trailer : unit -> unit + +val push_in_preamble : string -> unit + +val dump_file : string -> unit + +val start_module : unit -> unit + +val start_doc : unit -> unit +val end_doc : unit -> unit + +val start_coq : unit -> unit +val end_coq : unit -> unit + +val start_code : unit -> unit +val end_code : unit -> unit + +val start_inline_coq : unit -> unit +val end_inline_coq : unit -> unit + +val indentation : int -> unit +val line_break : unit -> unit +val paragraph : unit -> unit +val empty_line_of_code : unit -> unit + +val section : int -> (unit -> unit) -> unit + +val item : int -> unit + +val rule : unit -> unit + +val char : char -> unit +val ident : string -> loc -> unit +val symbol : string -> unit + +val latex_char : char -> unit +val latex_string : string -> unit +val html_char : char -> unit +val html_string : string -> unit +val verbatim_char : char -> unit +val hard_verbatim_char : char -> unit + +val start_latex_math : unit -> unit +val stop_latex_math : unit -> unit +val start_verbatim : unit -> unit +val stop_verbatim : unit -> unit + +val make_index : unit -> unit +val make_toc : unit -> unit |