diff options
| author | sacerdot | 2004-04-06 20:13:03 +0000 |
|---|---|---|
| committer | sacerdot | 2004-04-06 20:13:03 +0000 |
| commit | b62621f2c0ae08b65aca697f68b0595b53b976ff (patch) | |
| tree | cc9dab8151097bdabd06c443ff917dac4e88abc0 /tools | |
| 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')
| -rw-r--r-- | tools/coqdoc/output.ml | 31 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 1 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 11 |
3 files changed, 28 insertions, 15 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 615d22486e..cbb435f4aa 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 diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 0da9669420..84a85a7fc7 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -81,6 +81,7 @@ 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 diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 02a0a78487..7f5f782f07 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -400,6 +400,10 @@ and doc = parse { escaped_html lexbuf; doc lexbuf } | "##" { char '#'; doc lexbuf } + | "^" + { escaped lexbuf; doc lexbuf } + | "^^" + { char '^'; doc lexbuf } | eof { false } | _ @@ -426,6 +430,13 @@ and escaped_html = parse | eof { () } | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } +and escaped = parse + | "^" { () } + | "^^" + { hard_verbatim_char '^'; escaped lexbuf } + | eof { () } + | _ { hard_verbatim_char (lexeme_char lexbuf 0); escaped lexbuf } + and verbatim = parse | "\n>>" { verbatim_char '\n'; stop_verbatim () } | eof { stop_verbatim () } |