From b62621f2c0ae08b65aca697f68b0595b53b976ff Mon Sep 17 00:00:00 2001 From: sacerdot Date: Tue, 6 Apr 2004 20:13:03 +0000 Subject: 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 --- tools/coqdoc/output.ml | 31 ++++++++++++++++--------------- tools/coqdoc/output.mli | 1 + tools/coqdoc/pretty.mll | 11 +++++++++++ 3 files changed, 28 insertions(+), 15 deletions(-) (limited to 'tools') 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 "\n\n"; + printf "\n\n"; if !charset != "" then printf "" !charset; printf ""; @@ -333,9 +333,9 @@ module Html = struct let trailer () = if !index && !current_module <> "Index" then - printf "
Index"; + printf "
Index"; if !header_trailer then begin - printf "
This page has been generated by "; + printf "
This page has been generated by "; printf "coqdoc\n" self; printf "\n" end @@ -348,9 +348,9 @@ module Html = struct let indentation n = for i = 1 to n do printf " " done - let line_break () = printf "
\n" + let line_break () = printf "
\n" - let empty_line_of_code () = printf "\n
\n" + let empty_line_of_code () = printf "\n
\n" let char = function | '<' -> printf "<" @@ -430,14 +430,14 @@ module Html = struct printf "\n\n"; decr item_level; + printf "\n\n\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
  • " + if n <= old_level then printf "\n
    • \n
  • " let stop_item () = reach_item_level 0 @@ -461,7 +461,7 @@ module Html = struct let end_inline_coq () = printf "" - let paragraph () = stop_item (); printf "\n

    \n" + let paragraph () = stop_item (); printf "\n

    \n" let section lev f = let lab = new_label () in @@ -472,7 +472,7 @@ module Html = struct f (); printf "\n" lev - let rule () = printf "
    \n" + let rule () = printf "
    \n" let entry_type = function | Library -> "library" @@ -496,8 +496,8 @@ module Html = struct printf "

    %c %s

    \n" idx c c cat; List.iter (fun (id,(text,link)) -> - printf "%s %s
    \n" link id text) l; - printf "

    " + printf "%s %s
    \n" link id text) l; + printf "

    " 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 "
    "; + printf "
    "; letter_index true idx cl; - if List.length l > 30 then begin printf "
    "; navig () end; + if List.length l > 30 then begin printf "
    "; 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 "
    \n

    %s Index

    \n" (String.capitalize i.idx_name); + printf "
    \n

    %s Index

    \n" (String.capitalize i.idx_name); all_letters i end in List.iter one_index idxl; - printf "
    "; + printf "
    "; 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 () } -- cgit v1.2.3