aboutsummaryrefslogtreecommitdiffhomepage
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.css33
-rw-r--r--tools/coqdoc/main.ml3
-rw-r--r--tools/coqdoc/output.ml41
-rw-r--r--tools/coqdoc/output.mli3
-rw-r--r--tools/coqdoc/pretty.mll70
6 files changed, 119 insertions, 32 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5bcbed64e..c81dcec17 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -57,6 +57,7 @@ let externals = ref true
let coqlib = ref "http://coq.inria.fr/library/"
let coqlib_path = ref Coq_config.coqlib
let raw_comments = ref false
+let parse_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 a9a997066..762be5aff 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -57,6 +57,11 @@ body { padding: 0px 0px;
display: inline;
font-family: monospace }
+.comment {
+ display: inline;
+ font-family: monospace;
+ color: red; }
+
.code {
display: block;
font-family: monospace }
@@ -80,18 +85,46 @@ body { padding: 0px 0px;
color: rgb(40%,0%,40%);
}
+.id[type="variable"] {
+ color: rgb(40%,0%,40%);
+}
+
.id[type="definition"] {
color: rgb(0%,40%,0%);
}
+.id[type="abbreviation"] {
+ color: rgb(0%,40%,0%);
+}
+
.id[type="lemma"] {
color: rgb(0%,40%,0%);
}
+.id[type="instance"] {
+ color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] {
+ color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] {
+ color: rgb(0%,40%,0%);
+}
+
.id[type="inductive"] {
color: rgb(0%,0%,80%);
}
+.id[type="record"] {
+ color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] {
+ color: rgb(0%,0%,80%);
+}
+
.id[type="keyword"] {
color : #cf1d1d;
/* color: black; */
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 04f9ee4b0..24538360a 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -65,6 +65,7 @@ let usage () =
prerr_endline " --charset <string> set HTML charset";
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 "";
exit 1
@@ -273,6 +274,8 @@ let parse () =
usage ()
| ("-raw-comments" | "--raw-comments") :: rem ->
Cdglobals.raw_comments := true; parse_rec rem
+ | ("-parse-comments" | "--parse-comments") :: rem ->
+ Cdglobals.parse_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 568fade17..032c35caf 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -298,7 +298,7 @@ module Latex = struct
else
with_latex_printing (fun s -> ident s l) s
- let symbol = with_latex_printing raw_ident
+ let symbol s = with_latex_printing raw_ident s
let rec reach_item_level n =
if !item_level < n then begin
@@ -320,6 +320,12 @@ module Latex = struct
let end_doc () = in_doc := false; stop_item ()
+ let comment c = char c
+
+ let start_comment () = printf "\\begin{coqdoccomment}\n"
+
+ let end_comment () = printf "\\end{coqdoccomment}\n"
+
let start_coq () = printf "\\begin{coqdoccode}\n"
let end_coq () = printf "\\end{coqdoccode}\n"
@@ -456,14 +462,15 @@ module Html = struct
let ident_ref m fid typ s =
match find_module m with
| Local ->
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
printf "<span class=\"id\" type=\"%s\">" typ;
- printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
- printf "</a></span>"
+ raw_ident s;
+ printf "</span></a>"
| Coqlib when !externals ->
let m = Filename.concat !coqlib m in
- printf "<span class=\"id\" type=\"%s\">" typ;
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
- raw_ident s; printf "</a></span>"
+ printf "<span class=\"id\" type=\"%s\">" typ;
+ raw_ident s; printf "</span></a>"
| Coqlib | Unknown ->
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
@@ -477,8 +484,9 @@ module Html = struct
try
(match Index.find !current_module loc with
| Def (fullid,ty) ->
+ printf "<a name=\"%s\">" fullid;
printf "<span class=\"id\" type=\"%s\">" (type_name ty);
- printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
+ raw_ident s; printf "</span></a>"
| Mod (m,s') when s = s' ->
module_ref m s
| Ref (m,fullid,ty) ->
@@ -500,9 +508,11 @@ module Html = struct
with Not_found ->
f tok
- let ident s l = with_html_printing (fun s -> ident s l) s
+ let ident s l =
+ with_html_printing (fun s -> ident s l) s
- let symbol = with_html_printing raw_ident
+ let symbol s =
+ with_html_printing raw_ident s
let rec reach_item_level n =
if !item_level < n then begin
@@ -532,6 +542,10 @@ module Html = struct
stop_item ();
if not !raw_comments then printf "\n</div>\n"
+ let start_comment () = printf "<span class=\"comment\">(*"
+
+ let end_comment () = printf "*)</span>"
+
let start_code () = end_doc (); start_coq ()
let end_code () = end_coq (); start_doc ()
@@ -770,6 +784,9 @@ module TeXmacs = struct
let end_coq () = ()
+ let start_comment () = ()
+ let end_comment () = ()
+
let start_code () = in_doc := true; printf "<\\code>\n"
let end_code () = in_doc := false; printf "\n</code>"
@@ -849,7 +866,7 @@ module Raw = struct
let ident s loc = raw_ident s
- let symbol = raw_ident
+ let symbol s = raw_ident s
let item n = printf "- "
@@ -858,6 +875,9 @@ module Raw = struct
let start_doc () = printf "(** "
let end_doc () = printf " *)\n"
+ let start_comment () = ()
+ let end_comment () = ()
+
let start_coq () = ()
let end_coq () = ()
@@ -911,6 +931,9 @@ let start_module =
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_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
+let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
+
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
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index f8fbb0fa4..181ccf1ca 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -28,6 +28,9 @@ val start_module : unit -> unit
val start_doc : unit -> unit
val end_doc : unit -> unit
+val start_comment : unit -> unit
+val end_comment : unit -> unit
+
val start_coq : unit -> unit
val end_coq : unit -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 1480624a5..c69ac0495 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -162,6 +162,8 @@
else
String.sub s 1 (String.length s - 3)
+ let symbol lexbuf s = Output.symbol s
+
}
(*s Regular expressions *)
@@ -217,7 +219,10 @@ let thm_token =
| "Proposition"
| "Property"
| "Goal"
- | "Next" space+ "Obligation"
+
+let prf_token =
+ "Next" space+ "Obligation"
+ | "Proof" (space* "." | space+ "with")
let def_token =
"Definition"
@@ -307,7 +312,6 @@ let prog_kw =
let gallina_kw_to_hide =
"Implicit" space+ "Arguments"
- | "Next" "Obligation"
| "Ltac"
| "Require"
| "Import"
@@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
rule coq_bol = parse
| space* nl+
- { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
+ { if not (!in_proof && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
| space* "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
@@ -381,20 +385,20 @@ rule coq_bol = parse
let eol = body lexbuf in
in_proof := true;
if eol then coq_bol lexbuf else coq lexbuf }
- | space* "Proof" (space* "." | space+ "with")
+ | space* prf_token
{ in_proof := true;
let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body_bol lexbuf end
- else true
+ else let s = lexeme lexbuf in
+ if s.[String.length s - 1] = '.' then false
+ else skip_to_dot lexbuf
in if eol then coq_bol lexbuf else coq lexbuf }
| space* end_kw {
let eol =
if not (!in_proof && !Cdglobals.gallina) then
begin backtrack lexbuf; body_bol lexbuf end
- else
- let eol = skip_to_dot lexbuf in
- if eol then Output.line_break (); eol
+ else skip_to_dot lexbuf
in
in_proof := false;
if eol then coq_bol lexbuf else coq lexbuf }
@@ -442,6 +446,12 @@ rule coq_bol = parse
coq_bol lexbuf }
| space* "(*"
{ comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
let eol = comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| eof
@@ -467,12 +477,18 @@ and coq = parse
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
let eol = comment lexbuf in
- if eol then begin Output.line_break(); coq_bol lexbuf end
+ if eol then coq_bol lexbuf
else coq lexbuf
}
| nl+ space* "]]"
- { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
+ { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
| eof
{ () }
| gallina_kw_to_hide
@@ -492,9 +508,7 @@ and coq = parse
let eol =
if not (!in_proof && !Cdglobals.gallina) then
begin backtrack lexbuf; body lexbuf end
- else
- let eol = skip_to_dot lexbuf in
- if eol then Output.line_break (); eol
+ else skip_to_dot lexbuf
in
in_proof := false;
if eol then coq_bol lexbuf else coq lexbuf }
@@ -617,8 +631,7 @@ and escaped_coq = parse
{ () }
| token_brackets
{ let s = lexeme lexbuf in
- Output.symbol s;
- escaped_coq lexbuf }
+ symbol lexbuf s; escaped_coq lexbuf }
| (identifier '.')* identifier
{ Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
| _
@@ -646,11 +659,20 @@ and comments = parse
and comment = parse
| "(*" { incr comment_level; comment lexbuf }
- | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | eof { false }
- | _ { comment lexbuf }
-
+ | "*)" space* nl {
+ 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 }
+ | 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 }
+ | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+ comment lexbuf }
+
and skip_to_dot = parse
| '.' space* nl { true }
| eof | '.' space+ { false}
@@ -665,13 +687,15 @@ and body_bol = parse
and body = parse
| nl {Output.line_break(); body_bol lexbuf}
| nl+ space* "]]"
- { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
+ { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
| eof { false }
| '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }
| '.' space+ { Output.char '.'; Output.char ' '; false }
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
| "(*" { comment_level := 1;
+ if !Cdglobals.parse_comments then Output.start_comment ();
let eol = comment lexbuf in
+ if !Cdglobals.parse_comments then Output.end_comment ();
if eol
then begin Output.line_break(); body_bol lexbuf end
else body lexbuf }
@@ -681,7 +705,7 @@ and body = parse
body lexbuf }
| token_no_brackets
{ let s = lexeme lexbuf in
- Output.symbol s; body lexbuf }
+ symbol lexbuf s; body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
body lexbuf }
@@ -696,7 +720,7 @@ and notation = parse
| '"' { Output.char '"'}
| token
{ let s = lexeme lexbuf in
- Output.symbol s; notation lexbuf }
+ symbol lexbuf s; notation lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
notation lexbuf }
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 03:20:04 +0000