diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-31 16:13:58 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-31 16:13:58 +0000 |
commit | e06b69a83b8e109d029a73116039da2c4adb179d (patch) | |
tree | 44bf44cd68d6b066bf55f56a843d34ad0446e827 /tools | |
parent | e697a1ee04e201b90bab3783b40f52841ef12fc0 (diff) |
Ajout d'une option -raw pour Coqdoc (sortie en texte brut)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11529 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 4 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 159 |
3 files changed, 128 insertions, 37 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 772846f0b..5bcbed64e 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -10,7 +10,7 @@ (*s Output options *) -type target_language = LaTeX | HTML | TeXmacs +type target_language = LaTeX | HTML | TeXmacs | Raw let target_language = ref HTML diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 08707ba24..add43b7c0 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -30,6 +30,7 @@ let usage () = prerr_endline " --html produce a HTML document (default)"; prerr_endline " --latex produce a LaTeX document"; prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --raw produce a text document"; prerr_endline " --dvi output the DVI"; prerr_endline " --ps output the PostScript"; prerr_endline " --pdf output the Pdf"; @@ -82,6 +83,7 @@ let banner () = let target_full_name f = match !Cdglobals.target_language with | HTML -> f ^ ".html" + | Raw -> f ^ ".txt" | _ -> f ^ ".tex" (*s \textbf{Separation of files.} Files given on the command line are @@ -258,6 +260,8 @@ let parse () = Cdglobals.target_language := HTML; parse_rec rem | ("-texmacs" | "--texmacs") :: rem -> Cdglobals.target_language := TeXmacs; parse_rec rem + | ("-raw" | "--raw") :: rem -> + Cdglobals.target_language := Raw; parse_rec rem | ("-charset" | "--charset") :: s :: rem -> Cdglobals.charset := s; parse_rec rem | ("-charset" | "--charset") :: [] -> diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 70f9a849f..57ccce764 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -796,68 +796,155 @@ module TeXmacs = struct end + +(*s LaTeX output *) + +module Raw = struct + + let header () = () + + let trailer () = () + + let char = output_char + + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + + let latex_char = output_char + let latex_string = output_string + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = () + let end_module () = () + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = () + + let stop_verbatim () = () + + let indentation n = + for i = 1 to n do printf " " done + + let ident s loc = raw_ident s + + let symbol = raw_ident + + let item n = printf "- " + + let stop_item () = () + + let start_doc () = printf "(** " + let end_doc () = printf " *)\n" + + let start_coq () = () + let end_coq () = () + + let start_code () = end_doc (); start_coq () + let end_code () = end_coq (); start_doc () + + let section_kind = + function + | 1 -> "*" + | 2 -> "**" + | 3 -> "***" + | 4 -> "****" + | _ -> assert false + + let section lev f = + output_string (section_kind lev); + f () + + let rule () = () + + let paragraph () = printf "\n\n" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = () + let end_inline_coq () = () + + let make_multi_index () = () + let make_index () = () + let make_toc () = () + +end + + + (*s Generic output *) -let select f1 f2 f3 x = - match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x +let select f1 f2 f3 f4 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x let push_in_preamble = Latex.push_in_preamble -let header = select Latex.header Html.header TeXmacs.header -let trailer = select Latex.trailer Html.trailer TeXmacs.trailer +let header = select Latex.header Html.header TeXmacs.header Raw.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer let start_module = - select Latex.start_module Html.start_module TeXmacs.start_module + select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module -let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc -let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc +let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc -let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq -let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq +let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq -let start_code = select Latex.start_code Html.start_code TeXmacs.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code +let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code let start_inline_coq = - select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = - select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq -let indentation = select Latex.indentation Html.indentation TeXmacs.indentation -let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph -let line_break = select Latex.line_break Html.line_break TeXmacs.line_break +let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break let empty_line_of_code = select - Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code -let section = select Latex.section Html.section TeXmacs.section -let item = select Latex.item Html.item TeXmacs.item -let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item -let rule = select Latex.rule Html.rule TeXmacs.rule +let section = select Latex.section Html.section TeXmacs.section Raw.section +let item = select Latex.item Html.item TeXmacs.item Raw.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule -let char = select Latex.char Html.char TeXmacs.char -let ident = select Latex.ident Html.ident TeXmacs.ident -let symbol = select Latex.symbol Html.symbol TeXmacs.symbol +let char = select Latex.char Html.char TeXmacs.char Raw.char +let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol -let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char let latex_string = - select Latex.latex_string Html.latex_string TeXmacs.latex_string -let html_char = select Latex.html_char Html.html_char TeXmacs.html_char + select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char let html_string = - select Latex.html_string Html.html_string TeXmacs.html_string + select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string let start_latex_math = - select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = - select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math let start_verbatim = - select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim + select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim let stop_verbatim = - select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim let verbatim_char = - select output_char Html.char TeXmacs.char + select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char -let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index -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 +let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index +let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index +let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc |