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

1 files changed, 123 insertions, 36 deletions

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