1
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
2
(************************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
5
(* \VV/ **************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(************************************************************************)
10
(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
15
(*s Low level output *)
17
let output_char c = Pervasives.output_char !out_channel c
19
let output_string s = Pervasives.output_string !out_channel s
21
let printf s = Printf.fprintf !out_channel s
23
let sprintf = Printf.sprintf
29
let h = Hashtbl.create 101 in
30
List.iter (fun key ->Hashtbl.add h key ()) l;
31
function s -> try Hashtbl.find h s; true with Not_found -> false
35
[ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
36
"CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
37
"Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
38
"Hypothesis"; "Hypotheses";
39
"Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
40
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
41
"Module"; "Module Type"; "Declare Module"; "Include";
42
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
43
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
44
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
45
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
46
"Notation"; "Reserved Notation"; "Tactic Notation";
47
"Delimit"; "Bind"; "Open"; "Scope";
48
"Boxed"; "Unboxed"; "Inline";
49
"Implicit Arguments"; "Add"; "Strict";
50
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
53
"Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
54
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
55
"Program Instance"; "Equations"; "Equations_nocomp";
56
(*i (* coq terms *) *)
57
"forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun";
58
"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
65
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
66
"elimtype"; "progress"; "setoid_rewrite";
67
"destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
68
"f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
69
"set"; "assert"; "do"; "repeat";
70
"cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate";
71
"simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
72
"reflexivity"; "symmetry"; "transitivity";
73
"replace"; "setoid_replace"; "inversion"; "inversion_clear";
74
"pattern"; "intuition"; "congruence"; "fail"; "fresh";
75
"trivial"; "exact"; "tauto"; "firstorder"; "ring";
76
"clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
78
(*s Current Coq module *)
80
let current_module = ref ""
82
let set_module m = current_module := m; page_title := m
84
(*s Common to both LaTeX and HTML *)
86
let item_level = ref 0
88
(*s Customized pretty-print *)
90
let token_pp = Hashtbl.create 97
92
let add_printing_token = Hashtbl.replace token_pp
94
let find_printing_token tok =
95
try Hashtbl.find token_pp tok with Not_found -> None, None
97
let remove_printing_token = Hashtbl.remove token_pp
99
(* predefined pretty-prints *)
101
let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
103
(fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l'))
104
[ "*" , "\\ensuremath{\\times}", if_utf8 "×";
105
"|", "\\ensuremath{|}", None;
106
"->", "\\ensuremath{\\rightarrow}", if_utf8 "→";
107
"->~", "\\ensuremath{\\rightarrow\\lnot}", None;
108
"->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
109
"<-", "\\ensuremath{\\leftarrow}", None;
110
"<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
111
"=>", "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
112
"<=", "\\ensuremath{\\le}", if_utf8 "≤";
113
">=", "\\ensuremath{\\ge}", if_utf8 "≥";
114
"<>", "\\ensuremath{\\not=}", if_utf8 "≠";
115
"~", "\\ensuremath{\\lnot}", if_utf8 "¬";
116
"/\\", "\\ensuremath{\\land}", if_utf8 "∧";
117
"\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
118
"|-", "\\ensuremath{\\vdash}", None;
119
"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
120
"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
121
"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
122
"λ", "\\ensuremath{\\lambda}", if_utf8 "λ"
123
(* "fun", "\\ensuremath{\\lambda}" ? *)
126
(*s Table of contents *)
129
| Toc_library of string
130
| Toc_section of int * (unit -> unit) * string
132
let (toc_q : toc_entry Queue.t) = Queue.create ()
134
let add_toc_entry e = Queue.add e toc_q
136
let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
140
module Latex = struct
142
let in_title = ref false
143
let in_doc = ref false
145
(*s Latex preamble *)
147
let (preamble : string Queue.t) = Queue.create ()
149
let push_in_preamble s = Queue.add s preamble
152
if !header_trailer then begin
153
printf "\\documentclass[12pt]{report}\n";
154
if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
155
printf "\\usepackage[T1]{fontenc}\n";
156
printf "\\usepackage{fullpage}\n";
157
printf "\\usepackage{coqdoc}\n";
158
Queue.iter (fun s -> printf "%s\n" s) preamble;
159
printf "\\begin{document}\n"
162
"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
164
"%% This file has been automatically generated with the command\n";
166
Array.iter (fun s -> printf "%s " s) Sys.argv;
169
"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"
172
if !header_trailer then begin
173
printf "\\end{document}\n"
176
let char c = match c with
178
printf "\\symbol{92}"
179
| '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
180
output_char '\\'; output_char c
182
output_char '\\'; output_char c; printf "{}"
186
let label_char c = match c with
187
| '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
192
let latex_char = output_char
193
let latex_string = output_string
196
let html_string _ = ()
199
for i = 0 to String.length s - 1 do char s.[i] done
202
for i = 0 to String.length s - 1 do label_char s.[i] done
204
let start_module () =
205
if not !short then begin
206
printf "\\coqlibrary{";
207
label_ident !current_module;
209
raw_ident !current_module;
213
let start_latex_math () = output_char '$'
215
let stop_latex_math () = output_char '$'
217
let start_verbatim () = printf "\\begin{verbatim}"
219
let stop_verbatim () = printf "\\end{verbatim}\n"
223
printf "\\coqdocnoindent\n"
225
let space = 0.5 *. (float n) in
226
printf "\\coqdocindent{%2.2fem}\n" space
228
let with_latex_printing f tok =
230
(match Hashtbl.find token_pp tok with
231
| Some s, _ -> output_string s
237
printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
239
match find_module m with
241
printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
242
| Coqlib when !externals ->
243
let m = Filename.concat !coqlib m in
244
printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
245
| Coqlib | Unknown ->
249
let ident_ref m fid typ s =
250
let id = if fid <> "" then (m ^ "." ^ fid) else m in
251
match find_module m with
253
printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
254
| Coqlib when !externals ->
255
let _m = Filename.concat !coqlib m in
256
printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
257
| Coqlib | Unknown ->
258
printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
260
let defref m id ty s =
261
printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
263
let reference s = function
264
| Def (fullid,typ) ->
265
defref !current_module fullid typ s
266
| Mod (m,s') when s = s' ->
268
| Ref (m,fullid,typ) ->
269
ident_ref m fullid typ s
271
printf "\\coqdocvar{"; raw_ident s; printf "}"
274
if is_keyword s then begin
275
printf "\\coqdockw{"; raw_ident s; printf "}"
279
reference s (Index.find !current_module loc)
281
if is_tactic s then begin
282
printf "\\coqdoctac{"; raw_ident s; printf "}"
284
if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
286
try reference s (Index.find_string !current_module s)
287
with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
288
else (printf "\\coqdocvar{"; raw_ident s; printf "}")
295
printf "\\texorpdfstring{\\protect";
296
with_latex_printing (fun s -> ident s l) s;
297
printf "}{"; raw_ident s; printf "}")
299
with_latex_printing (fun s -> ident s l) s
301
let symbol s = with_latex_printing raw_ident s
303
let rec reach_item_level n =
304
if !item_level < n then begin
305
printf "\n\\begin{itemize}\n\\item "; incr item_level;
307
end else if !item_level > n then begin
308
printf "\n\\end{itemize}\n"; decr item_level;
313
let old_level = !item_level in
315
if n <= old_level then printf "\n\\item "
317
let stop_item () = reach_item_level 0
319
let start_doc () = in_doc := true
321
let end_doc () = in_doc := false; stop_item ()
323
let comment c = char c
325
let start_comment () = printf "\\begin{coqdoccomment}\n"
327
let end_comment () = printf "\\end{coqdoccomment}\n"
329
let start_coq () = printf "\\begin{coqdoccode}\n"
331
let end_coq () = printf "\\end{coqdoccode}\n"
333
let start_code () = end_doc (); start_coq ()
335
let end_code () = end_coq (); start_doc ()
337
let section_kind = function
339
| 2 -> "\\subsection{"
340
| 3 -> "\\subsubsection{"
341
| 4 -> "\\paragraph{"
346
output_string (section_kind lev);
347
in_title := true; f (); in_title := false;
351
printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
353
let paragraph () = stop_item (); printf "\n\n"
355
let line_break () = printf "\\coqdoceol\n"
357
let empty_line_of_code () = printf "\\coqdocemptyline\n"
359
let start_inline_coq () = ()
361
let end_inline_coq () = ()
363
let make_multi_index () = ()
365
let make_index () = ()
367
let make_toc () = printf "\\tableofcontents\n"
377
if !header_trailer then
378
if !header_file_spec then
379
let cin = Pervasives.open_in !header_file in
382
let s = Pervasives.input_line cin in
385
with End_of_file -> Pervasives.close_in cin
388
printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
389
printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
390
printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
391
printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
392
printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
393
printf "<title>%s</title>\n</head>\n\n" !page_title;
394
printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
395
printf "<div id=\"main\">\n\n"
399
if !index && !current_module <> "Index" then
400
printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
401
if !header_trailer then
402
if !footer_file_spec then
403
let cin = Pervasives.open_in !footer_file in
406
let s = Pervasives.input_line cin in
409
with End_of_file -> Pervasives.close_in cin
412
printf "<hr/>This page has been generated by ";
413
printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
414
printf "</div>\n\n</div>\n\n</body>\n</html>"
417
let start_module () =
418
if not !short then begin
419
add_toc_entry (Toc_library !current_module);
420
printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
423
let indentation n = for i = 1 to n do printf " " done
425
let line_break () = printf "<br/>\n"
427
let empty_line_of_code () =
431
| '<' -> printf "<"
432
| '>' -> printf ">"
433
| '&' -> printf "&"
436
let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done
438
let latex_char _ = ()
439
let latex_string _ = ()
441
let html_char = output_char
442
let html_string = output_string
444
let start_latex_math () = ()
445
let stop_latex_math () = ()
447
let start_verbatim () = printf "<pre>"
448
let stop_verbatim () = printf "</pre>\n"
451
match find_module m with
453
printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
454
| Coqlib when !externals ->
455
let m = Filename.concat !coqlib m in
456
printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
457
| Coqlib | Unknown ->
460
let ident_ref m fid typ s =
461
match find_module m with
463
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
464
printf "<span class=\"id\" type=\"%s\">" typ;
467
| Coqlib when !externals ->
468
let m = Filename.concat !coqlib m in
469
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
470
printf "<span class=\"id\" type=\"%s\">" typ;
471
raw_ident s; printf "</span></a>"
472
| Coqlib | Unknown ->
473
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
476
if is_keyword s then begin
477
printf "<span class=\"id\" type=\"keyword\">";
483
(match Index.find !current_module loc with
485
printf "<a name=\"%s\">" fullid;
486
printf "<span class=\"id\" type=\"%s\">" (type_name ty);
487
raw_ident s; printf "</span></a>"
488
| Mod (m,s') when s = s' ->
490
| Ref (m,fullid,ty) ->
491
ident_ref m fullid (type_name ty) s
493
printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
496
(printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
498
(printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
501
let with_html_printing f tok =
503
(match Hashtbl.find token_pp tok with
504
| _, Some s -> output_string s
510
with_html_printing (fun s -> ident s l) s
513
with_html_printing raw_ident s
515
let rec reach_item_level n =
516
if !item_level < n then begin
517
printf "\n<ul>\n<li>"; incr item_level;
519
end else if !item_level > n then begin
520
printf "\n</li>\n</ul>\n"; decr item_level;
525
let old_level = !item_level in
527
if n <= old_level then printf "\n</li>\n<li>"
529
let stop_item () = reach_item_level 0
531
let start_coq () = if not !raw_comments then printf "<div class=\"code\">\n"
533
let end_coq () = if not !raw_comments then printf "</div>\n"
536
if not !raw_comments then
537
printf "\n<div class=\"doc\">\n"
541
if not !raw_comments then printf "\n</div>\n"
543
let start_comment () = printf "<span class=\"comment\">(*"
545
let end_comment () = printf "*)</span>"
547
let start_code () = end_doc (); start_coq ()
549
let end_code () = end_coq (); start_doc ()
551
let start_inline_coq () = printf "<span class=\"inlinecode\">"
553
let end_inline_coq () = printf "</span>"
556
let i = !item_level in
558
if i > 0 then printf "\n"
559
else printf "\n<br/> <br/>\n"
562
let lab = new_label () in
563
let r = sprintf "%s.html#%s" !current_module lab in
564
add_toc_entry (Toc_section (lev, f, r));
566
printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
568
printf "</h%d>\n" lev
570
let rule () = printf "<hr/>\n"
572
(* make a HTML index from a list of triples (name,text,link) *)
574
let idxc = sprintf "%s_%c" i.idx_name c in
575
if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc
577
let letter_index category idx (c,l) =
578
if l <> [] then begin
579
let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
580
printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat;
582
(fun (id,(text,link)) ->
583
printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
587
let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
589
(* Construction d'une liste des index (1 index global, puis 1
590
index par catégorie) *)
591
let format_global_index =
595
"[library]", m ^ ".html"
597
sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
598
sprintf "%s.html#%s" m s)
600
let format_bytype_index = function
602
Index.map (fun id m -> "", m ^ ".html") idx
606
let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
607
(text, sprintf "%s.html#%s" m s)) idx
609
(* Impression de la table d'index *)
610
let print_index_table_item i =
611
printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
615
printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
617
printf "<td>%c</td>\n" c)
619
let n = i.idx_size in
620
printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
623
let print_index_table idxl =
625
List.iter print_index_table_item idxl;
628
let make_one_multi_index prt_tbl i =
629
(* Attn: make_one_multi_index créé un nouveau fichier... *)
630
let idx = i.idx_name in
631
let one_letter ((c,l) as cl) =
632
open_out_file (sprintf "index_%s_%c.html" idx c);
633
if (!header_trailer) then header ();
634
prt_tbl (); printf "<hr/>";
635
letter_index true idx cl;
636
if List.length l > 30 then begin printf "<hr/>"; prt_tbl () end;
637
if (!header_trailer) then trailer ();
640
List.iter one_letter i.idx_entries
642
let make_multi_index () =
644
let glob,bt = Index.all_entries () in
645
(format_global_index glob) ::
646
(List.map format_bytype_index bt) in
647
let print_table () = print_index_table all_index in
648
List.iter (make_one_multi_index print_table) all_index
652
let glob,bt = Index.all_entries () in
653
(format_global_index glob) ::
654
(List.map format_bytype_index bt) in
655
let print_table () = print_index_table all_index in
656
let print_one_index i =
657
if i.idx_size > 0 then begin
658
printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
662
current_module := "Index";
663
if !title <> "" then printf "<h1>%s</h1>\n" !title;
665
if not (!multi_index) then
667
List.iter print_one_index all_index;
668
printf "<hr/>"; print_table ()
672
let make_toc_entry = function
675
printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
676
| Toc_section (n, f, r) ->
678
printf "<a href=\"%s\">" r; f (); printf "</a>\n"
680
Queue.iter make_toc_entry toc_q;
686
(*s TeXmacs-aware output *)
688
module TeXmacs = struct
690
(*s Latex preamble *)
692
let in_doc = ref false
694
let (preamble : string Queue.t) =
695
in_doc := false; Queue.create ()
697
let push_in_preamble s = Queue.add s preamble
701
"(*i This file has been automatically generated with the command \n";
703
" "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n"
707
let char_true c = match c with
708
| '\\' -> printf "\\\\"
709
| '<' -> printf "\\<"
710
| '|' -> printf "\\|"
711
| '>' -> printf "\\>"
714
let char c = if !in_doc then char_true c else output_char c
716
let latex_char = char_true
717
let latex_string = String.iter latex_char
720
let html_string _ = ()
723
for i = 0 to String.length s - 1 do char s.[i] done
725
let start_module () = ()
727
let start_latex_math () = printf "<with|mode|math|"
729
let stop_latex_math () = output_char '>'
731
let start_verbatim () = in_doc := true; printf "<\\verbatim>"
733
let stop_verbatim () = in_doc := false; printf "</verbatim>"
735
let indentation n = ()
738
if is_keyword s then begin
739
printf "<kw|"; raw_ident s; printf ">"
744
let ident s _ = if !in_doc then ident_true s else raw_ident s
747
let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in
749
| "*" -> ensuremath "times"
750
| "->" -> ensuremath "rightarrow"
751
| "<-" -> ensuremath "leftarrow"
752
| "<->" ->ensuremath "leftrightarrow"
753
| "=>" -> ensuremath "Rightarrow"
754
| "<=" -> ensuremath "le"
755
| ">=" -> ensuremath "ge"
756
| "<>" -> ensuremath "noteq"
757
| "~" -> ensuremath "lnot"
758
| "/\\" -> ensuremath "land"
759
| "\\/" -> ensuremath "lor"
760
| "|-" -> ensuremath "vdash"
763
let symbol s = if !in_doc then symbol_true s else raw_ident s
765
let rec reach_item_level n =
766
if !item_level < n then begin
767
printf "\n<\\itemize>\n<item>"; incr item_level;
769
end else if !item_level > n then begin
770
printf "\n</itemize>"; decr item_level;
775
let old_level = !item_level in
777
if n <= old_level then printf "\n\n<item>"
779
let stop_item () = reach_item_level 0
781
let start_doc () = in_doc := true; printf "(** texmacs: "
783
let end_doc () = stop_item (); in_doc := false; printf " *)"
785
let start_coq () = ()
789
let start_comment () = ()
790
let end_comment () = ()
792
let start_code () = in_doc := true; printf "<\\code>\n"
793
let end_code () = in_doc := false; printf "\n</code>"
795
let section_kind = function
798
| 3 -> "subsubsection"
804
printf "<"; output_string (section_kind lev); printf "|";
810
let paragraph () = stop_item (); printf "\n\n"
812
let line_break_true () = printf "<format|line break>"
814
let line_break () = printf "\n"
816
let empty_line_of_code () = printf "\n"
818
let start_inline_coq () = printf "<verbatim|["
820
let end_inline_coq () = printf "]>"
822
let make_multi_index () = ()
824
let make_index () = ()
839
let char = output_char
841
let label_char c = match c with
842
| '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
847
let latex_char = output_char
848
let latex_string = output_string
851
let html_string _ = ()
854
for i = 0 to String.length s - 1 do char s.[i] done
856
let start_module () = ()
857
let end_module () = ()
859
let start_latex_math () = ()
860
let stop_latex_math () = ()
862
let start_verbatim () = ()
864
let stop_verbatim () = ()
867
for i = 1 to n do printf " " done
869
let ident s loc = raw_ident s
871
let symbol s = raw_ident s
873
let item n = printf "- "
875
let stop_item () = ()
877
let start_doc () = printf "(** "
878
let end_doc () = printf " *)\n"
880
let start_comment () = ()
881
let end_comment () = ()
883
let start_coq () = ()
886
let start_code () = end_doc (); start_coq ()
887
let end_code () = end_coq (); start_doc ()
898
output_string (section_kind lev);
903
let paragraph () = printf "\n\n"
905
let line_break () = printf "\n"
907
let empty_line_of_code () = printf "\n"
909
let start_inline_coq () = ()
910
let end_inline_coq () = ()
912
let make_multi_index () = ()
913
let make_index () = ()
920
(*s Generic output *)
922
let select f1 f2 f3 f4 x =
923
match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x
925
let push_in_preamble = Latex.push_in_preamble
927
let header = select Latex.header Html.header TeXmacs.header Raw.header
928
let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer
931
select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module
933
let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
934
let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
936
let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
937
let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
939
let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
940
let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
942
let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
943
let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
945
let start_inline_coq =
946
select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
948
select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
950
let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
951
let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
952
let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
953
let empty_line_of_code = select
954
Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code
956
let section = select Latex.section Html.section TeXmacs.section Raw.section
957
let item = select Latex.item Html.item TeXmacs.item Raw.item
958
let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item
959
let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
961
let char = select Latex.char Html.char TeXmacs.char Raw.char
962
let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
963
let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
965
let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
967
select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
968
let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char
970
select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
972
let start_latex_math =
973
select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
974
let stop_latex_math =
975
select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math
978
select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
980
select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
982
select output_char Html.char TeXmacs.char Raw.char
983
let hard_verbatim_char = output_char
985
let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
986
let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
987
let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc
added
removed
tools/coqdoc/output.ml
