aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/cdglobals.ml1
-rw-r--r--tools/coqdoc/coqdoc.css1
-rw-r--r--tools/coqdoc/cpretty.mll98
-rw-r--r--tools/coqdoc/main.ml3
-rw-r--r--tools/coqdoc/output.ml9
5 files changed, 85 insertions, 27 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index b3f0739d19..7e074802de 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -58,6 +58,7 @@ let coqlib = ref Coq_config.wwwstdlib
let coqlib_path = ref Coq_config.coqlib
let raw_comments = ref false
let parse_comments = ref false
+let plain_comments = ref false
let interpolate = ref false
let charset = ref "iso-8859-1"
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 762be5aff6..b82caa7092 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -23,7 +23,6 @@ body { padding: 0px 0px;
#main{ display: block;
padding: 10px;
- overflow: hidden;
font-size: 100%;
line-height: 100% }
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 5ca970f353..83639402fb 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -577,30 +577,40 @@ and doc = parse
| nl
{ Output.char '\n'; doc_bol lexbuf }
| "[[" nl
- { formatted := true; Output.line_break (); Output.start_inline_coq ();
- let eol = body_bol lexbuf in
- Output.end_inline_coq (); formatted := false;
- if eol then doc_bol lexbuf else doc lexbuf}
+ { if !Cdglobals.plain_comments
+ then (Output.char '['; Output.char '['; doc lexbuf)
+ else (formatted := true;
+ Output.line_break (); Output.start_inline_coq ();
+ let eol = body_bol lexbuf in
+ Output.end_inline_coq (); formatted := false;
+ if eol then doc_bol lexbuf else doc lexbuf)}
| "["
- { brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
- doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '['
+ else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf;
+ Output.end_inline_coq ()); doc lexbuf }
| '*'* "*)" space* nl
{ true }
| '*'* "*)"
{ false }
| "$"
- { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '$'
+ else (Output.start_latex_math (); escaped_math_latex lexbuf);
+ doc lexbuf }
| "$$"
- { Output.char '$'; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '$';
+ Output.char '$'; doc lexbuf }
| "%"
- { escaped_latex lexbuf; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '%'
+ else escaped_latex lexbuf; doc lexbuf }
| "%%"
- { Output.char '%'; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '%';
+ Output.char '%'; doc lexbuf }
| "#"
- { escaped_html lexbuf; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '#'
+ else escaped_html lexbuf; doc lexbuf }
| "##"
- { Output.char '#'; doc lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '#';
+ Output.char '#'; doc lexbuf }
| eof
{ false }
| _
@@ -628,7 +638,7 @@ and escaped_html = parse
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
and verbatim = parse
- | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
+ | nl ">>" space* nl? { Output.verbatim_char '\n'; Output.stop_verbatim () }
| eof { Output.stop_verbatim () }
| _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
@@ -679,22 +689,64 @@ and comment = parse
if !Cdglobals.parse_comments then Output.start_comment ();
comment lexbuf }
| "*)" space* nl {
- if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ());
+ if !Cdglobals.parse_comments then
+ (Output.end_comment (); Output.line_break ());
decr comment_level; if !comment_level > 0 then comment lexbuf else true }
| "*)" {
if !Cdglobals.parse_comments then (Output.end_comment ());
decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | "[" {
- if !Cdglobals.parse_comments then (
- brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
+ | "[" {
+ if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then Output.char '['
+ else (brackets := 1; Output.start_inline_coq ();
+ escaped_coq lexbuf; Output.end_inline_coq ());
comment lexbuf }
+ | "[[" {
+ if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+ else (formatted := true;
+ Output.line_break (); Output.start_inline_coq ();
+ let _ = body_bol lexbuf in
+ Output.end_inline_coq (); formatted := false);
+ comment lexbuf}
+ | "$"
+ { if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then Output.char '$'
+ else (Output.start_latex_math (); escaped_math_latex lexbuf);
+ comment lexbuf }
+ | "$$"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
+ doc lexbuf }
+ | "%"
+ { if !Cdglobals.parse_comments
+ then
+ if !Cdglobals.plain_comments then Output.char '%'
+ else escaped_latex lexbuf; comment lexbuf }
+ | "%%"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '%'; Output.char '%');
+ comment lexbuf }
+ | "#"
+ { if !Cdglobals.parse_comments
+ then
+ if !Cdglobals.plain_comments then Output.char '$'
+ else escaped_html lexbuf; comment lexbuf }
+ | "##"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '#'; Output.char '#');
+ comment lexbuf }
| eof { false }
- | space+ { if !Cdglobals.parse_comments then
- Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
- | nl { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+ | space+ { if !Cdglobals.parse_comments
+ then Output.indentation (fst (count_spaces (lexeme lexbuf)));
+ comment lexbuf }
+ | nl { if !Cdglobals.parse_comments
+ then Output.line_break (); comment lexbuf }
| _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
- comment lexbuf }
+ comment lexbuf }
and skip_to_dot = parse
| '.' space* nl { true }
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index da65466ddf..301f4bdf70 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -66,6 +66,7 @@ let usage () =
prerr_endline " --inputenc <string> set LaTeX input encoding";
prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module";
prerr_endline " --parse-comments parse regular comments";
+ prerr_endline " --plain-comments consider comments as non-literate text";
prerr_endline "";
exit 1
@@ -276,6 +277,8 @@ let parse () =
Cdglobals.raw_comments := true; parse_rec rem
| ("-parse-comments" | "--parse-comments") :: rem ->
Cdglobals.parse_comments := true; parse_rec rem
+ | ("-plain-comments" | "--plain-comments") :: rem ->
+ Cdglobals.plain_comments := true; parse_rec rem
| ("-interpolate" | "--interpolate") :: rem ->
Cdglobals.interpolate := true; parse_rec rem
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 9fda0d0cad..b69e8b3695 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -668,14 +668,17 @@ module Html = struct
printf "<hr/>"; print_table ()
end
- let make_toc () =
+
+ let make_toc () =
let make_toc_entry = function
| Toc_library m ->
stop_item ();
printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
| Toc_section (n, f, r) ->
- item n;
- printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+ if n <= 3 then begin
+ item n;
+ printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+ end
in
Queue.iter make_toc_entry toc_q;
stop_item ();
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:24:45 +0000