diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-06 20:13:03 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-06 20:13:03 +0000 |
| commit | b62621f2c0ae08b65aca697f68b0595b53b976ff (patch) | |
| tree | cc9dab8151097bdabd06c443ff917dac4e88abc0 /tools/coqdoc/output.ml | |
| parent | cd902906499c85cf8af69ecb44f4960750de2771 (diff) | |
1. In -html mode the generated files are well-formed XML files
(i.e. the output is no longer HTML but (X)HTML)
2. Added (** ^ ... ^ *) to output verbatim characters that are NOT
quoted (whereas (** # ... # *) and all the other similar marks
do quote the characters according to the output language quoting
conventions).
3. Added ^^ to output a single '^' character
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5647 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 615d22486..cbb435f4a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -321,7 +321,7 @@ module Html = struct let header () = if !header_trailer then begin - printf "<html>\n<head>\n"; + printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n"; if !charset != "" then printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\">" !charset; printf "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">"; @@ -333,9 +333,9 @@ module Html = struct let trailer () = if !index && !current_module <> "Index" then - printf "<hr><a href=\"index.html\">Index</a>"; + printf "<hr/><a href=\"index.html\">Index</a>"; if !header_trailer then begin - printf "<hr><font size=\"-1\">This page has been generated by "; + printf "<hr/><font size=\"-1\">This page has been generated by "; printf "<a href=\"%s\">coqdoc</a></font>\n" self; printf "</body>\n</html>" end @@ -348,9 +348,9 @@ module Html = struct let indentation n = for i = 1 to n do printf " " done - let line_break () = printf "<br>\n" + let line_break () = printf "<br/>\n" - let empty_line_of_code () = printf "\n<br>\n" + let empty_line_of_code () = printf "\n<br/>\n" let char = function | '<' -> printf "<" @@ -430,14 +430,14 @@ module Html = struct printf "\n<ul>\n<li>"; incr item_level; reach_item_level n end else if !item_level > n then begin - printf "\n</ul>\n"; decr item_level; + printf "\n</li>\n</ul>\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; - if n <= old_level then printf "\n<li>" + if n <= old_level then printf "\n</li>\n<li>" let stop_item () = reach_item_level 0 @@ -461,7 +461,7 @@ module Html = struct let end_inline_coq () = printf "</code>" - let paragraph () = stop_item (); printf "\n<br><br>\n" + let paragraph () = stop_item (); printf "\n<br/><br/>\n" let section lev f = let lab = new_label () in @@ -472,7 +472,7 @@ module Html = struct f (); printf "</h%d>\n" lev - let rule () = printf "<hr>\n" + let rule () = printf "<hr/>\n" let entry_type = function | Library -> "library" @@ -496,8 +496,8 @@ module Html = struct printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat; List.iter (fun (id,(text,link)) -> - printf "<a href=\"%s\">%s</a> %s<br>\n" link id text) l; - printf "<br><br>" + printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l; + printf "<br/><br/>" end let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries @@ -508,9 +508,9 @@ module Html = struct set_out_file (sprintf "index_%s_%c.html" idx c); header (); navig (); - printf "<hr>"; + printf "<hr/>"; letter_index true idx cl; - if List.length l > 30 then begin printf "<hr>"; navig () end; + if List.length l > 30 then begin printf "<hr/>"; navig () end; trailer (); close () in @@ -573,12 +573,12 @@ module Html = struct end else begin let one_index i = if i.idx_size > 0 then begin - printf "<hr>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name); + printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name); all_letters i end in List.iter one_index idxl; - printf "<hr>"; + printf "<hr/>"; navig (); trailer (); close () @@ -806,6 +806,7 @@ let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim let verbatim_char = select output_char Html.char TeXmacs.char +let hard_verbatim_char = output_char let make_index = select Latex.make_index Html.make_index TeXmacs.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc |