aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/cdglobals.ml2
-rw-r--r--tools/coqdoc/main.ml4
-rw-r--r--tools/coqdoc/output.ml159
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 14:09:47 +0000