From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tools/coqdoc/output.mli | 92 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) create mode 100644 tools/coqdoc/output.mli (limited to 'tools/coqdoc/output.mli') 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 *) +(* 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 -- cgit v1.2.3