aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tools/coqdoc/cdglobals.ml5
-rw-r--r--tools/coqdoc/coqdoc.css128
-rw-r--r--tools/coqdoc/coqdoc.sty6
-rw-r--r--tools/coqdoc/cpretty.mli1
-rw-r--r--tools/coqdoc/cpretty.mll347
-rw-r--r--tools/coqdoc/index.mll10
-rw-r--r--tools/coqdoc/main.ml37
-rw-r--r--tools/coqdoc/output.ml213
-rw-r--r--tools/coqdoc/output.mli8
9 files changed, 622 insertions, 133 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 7e074802de..2ee90820f3 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -50,6 +50,7 @@ let gallina = ref false
let short = ref false
let index = ref true
let multi_index = ref false
+let index_name = ref "index"
let toc = ref false
let page_title = ref ""
let title = ref ""
@@ -59,6 +60,9 @@ let coqlib_path = ref Coq_config.coqlib
let raw_comments = ref false
let parse_comments = ref false
let plain_comments = ref false
+let toc_depth = (ref None : int option ref)
+let lib_name = ref "Library"
+let lib_subtitles = ref false
let interpolate = ref false
let charset = ref "iso-8859-1"
@@ -83,4 +87,3 @@ type coq_module = string
type file =
| Vernac_file of string * coq_module
| Latex_file of string
-
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index b82caa7092..24b514b764 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -19,13 +19,16 @@ body { padding: 0px 0px;
margin: 0;}
-/* Contenu */
+/* Contents */
#main{ display: block;
padding: 10px;
+ font-family: sans-serif;
font-size: 100%;
line-height: 100% }
+#main h1 { line-height: 95% } /* allow for multi-line headers */
+
#main a.idref:visited {color : #416DFF; text-decoration : none; }
#main a.idref:link {color : #416DFF; text-decoration : none; }
#main a.idref:hover {text-decoration : none; }
@@ -39,41 +42,93 @@ body { padding: 0px 0px;
#main .keyword { color : #cf1d1d }
#main { color: black }
-#main .section { background-color:#90bdff;
- font-size : 175% }
+.section { background-color: rgb(60%,60%,100%);
+ padding-top: 13px;
+ padding-bottom: 13px;
+ padding-left: 3px;
+ margin-top: 5px;
+ margin-bottom: 5px;
+ font-size : 175% }
+
+h2.section { background-color: rgb(80%,80%,100%);
+ padding-left: 3px;
+ padding-top: 12px;
+ padding-bottom: 10px;
+ font-size : 130% }
+
+h3.section { background-color: rgb(90%,90%,100%);
+ padding-left: 3px;
+ padding-top: 7px;
+ padding-bottom: 7px;
+ font-size : 115% }
+
+h4.section {
+/*
+ background-color: rgb(80%,80%,80%);
+ max-width: 20em;
+ padding-left: 5px;
+ padding-top: 5px;
+ padding-bottom: 5px;
+*/
+ background-color: white;
+ padding-left: 0px;
+ padding-top: 0px;
+ padding-bottom: 0px;
+ font-size : 100%;
+ font-style : bold;
+ text-decoration : underline;
+ }
#main .doc { margin: 0px;
- padding: 10px;
font-family: sans-serif;
font-size: 100%;
- line-height: 100%;
- font-weight:bold;
+ line-height: 125%;
+ max-width: 40em;
color: black;
+ padding: 10px;
background-color: #90bdff;
border-style: plain}
.inlinecode {
display: inline;
+/* font-size: 125%; */
+ color: #666666;
+ font-family: monospace }
+
+.doc .inlinecode {
+ display: inline;
+ font-size: 120%;
+ color: rgb(30%,30%,70%);
+ font-family: monospace }
+
+.doc .inlinecode .id {
+ color: rgb(30%,30%,70%);
+}
+
+.doc .code {
+ display: inline;
+ font-size: 120%;
+ color: rgb(30%,30%,70%);
font-family: monospace }
.comment {
display: inline;
font-family: monospace;
- color: red; }
+ color: rgb(50%,50%,80%);
+}
.code {
display: block;
- font-family: monospace }
+/* padding-left: 15px; */
+ font-size: 110%;
+ font-family: monospace;
+ }
/* Pied de page */
#footer { font-size: 65%;
font-family: sans-serif; }
-#footer a:visited { color: blue; }
-#footer a:link { text-decoration: none;
- color: #888888; }
-
.id { display: inline; }
.id[type="constructor"] {
@@ -128,3 +183,52 @@ body { padding: 0px 0px;
color : #cf1d1d;
/* color: black; */
}
+
+.inlinecode .id {
+ color: rgb(0%,0%,0%);
+}
+
+
+/* TOC */
+
+#toc h2 {
+ padding: 10px;
+ background-color: rgb(60%,60%,100%);
+}
+
+#toc li {
+ padding-bottom: 8px;
+}
+
+/* Index */
+
+#index {
+ margin: 0;
+ padding: 0;
+ width: 100%;
+}
+
+#index #frontispiece {
+ margin: 1em auto;
+ padding: 1em;
+ width: 60%;
+}
+
+.booktitle { font-size : 140% }
+.authors { font-size : 90%;
+ line-height: 115%; }
+.moreauthors { font-size : 60% }
+
+#index #entrance {
+ text-align: center;
+}
+
+#index #entrance .spacer {
+ margin: 0 30px 0 30px;
+}
+
+#index #footer {
+ position: absolute;
+ bottom: 0;
+ text-align: bottom;
+} \ No newline at end of file
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index fca9a1d769..32e635240d 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -103,14 +103,14 @@
\newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
\newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
\newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
- \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
- \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}}
+ \newcommand{\coqlibrary}[3]{\cleardoublepage\phantomsection
+ \hypertarget{coq:#1}{\chapter{#2\texorpdfstring{\coqdoccst}{}{#3}}}}
\else
\newcommand{\coqdef}[3]{#3}
\newcommand{\coqref}[2]{#2}
\newcommand{\texorpdfstring}[2]{#1}
\newcommand{\identref}[2]{\textsf{#2}}
- \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
+ \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
\fi
\usepackage{xr}
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index f02a79be50..213c76aafd 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -11,3 +11,4 @@
open Index
val coq_file : string -> Cdglobals.coq_module -> unit
+val detect_subtitle : string -> Cdglobals.coq_module -> string option
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 83639402fb..3ad9000503 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -13,7 +13,14 @@
{
open Printf
- open Lexing
+ open Lexing
+
+ (* A list function we need *)
+ let rec take n ls =
+ if n = 0 then [] else
+ match ls with
+ | [] -> []
+ | (l :: ls) -> l :: (take (n-1) ls)
(* count the number of spaces at the beginning of a string *)
let count_spaces s =
@@ -60,6 +67,15 @@
let in_proof = ref None
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
+ let backtrack_past_newline lexbuf =
+ let buf = lexeme lexbuf in
+ let splits = Str.bounded_split_delim (Str.regexp "['\n']") buf 2 in
+ match splits with
+ | [] -> ()
+ | (_ :: []) -> ()
+ | (s1 :: rest :: _) ->
+ let length_skip = 1 + String.length s1 in
+ lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
@@ -118,6 +134,62 @@
end else
true
+ (* for item lists *)
+ type list_compare =
+ | Before
+ | StartLevel of int
+ | InLevel of int * bool
+
+ (* Before : we're before any levels
+ StartLevel : at the same column as the dash in a level
+ InLevel : after the dash of this level, but before any deeper dashes.
+ bool is true if this is the last level *)
+ let find_level levels cur_indent =
+ match levels with
+ | [] -> Before
+ | (l::ls) ->
+ if cur_indent < l then Before
+ else
+ (* cur_indent will never be less than the head of the list *)
+ let rec findind ls n =
+ match ls with
+ | [] -> InLevel (n,true)
+ | (l :: []) -> if cur_indent = l then StartLevel n
+ else InLevel (n,true)
+ | (l1 :: l2 :: ls) ->
+ if cur_indent = l1 then StartLevel n
+ else if cur_indent < l2 then InLevel (n,false)
+ else findind (l2 :: ls) (n+1)
+ in
+ findind (l::ls) 1
+
+ type is_start_list =
+ | Rule
+ | List of int
+ | Neither
+
+ let check_start_list str =
+ let n_dashes = count_dashes str in
+ let (n_spaces,_) = count_spaces str in
+ if n_dashes >= 4 then
+ Rule
+ else
+ if n_dashes = 1 then
+ List n_spaces
+ else
+ Neither
+
+ (* examine a string for subtitleness *)
+ let subtitle m s =
+ match Str.split_delim (Str.regexp ":") s with
+ | [] -> false
+ | (name::_) ->
+ if (cut_head_tail_spaces name) = m then
+ true
+ else
+ false
+
+
(* tokens pretty-print *)
let token_buffer = Buffer.create 1024
@@ -192,6 +264,15 @@ let pfx_id = (id '.')*
let identifier =
id | pfx_id id
+(* This misses unicode stuff, and it adds "[" and "]". It's only an
+ approximation of idents - used for detecting whether an underscore
+ is part of an identifier or meant to indicate emphasis *)
+let nonidentchar =
+ [^ 'A'-'Z' 'a'-'z' '_' '[' ']'
+ (* iso 8859-1 accents *)
+ '\192'-'\214' '\216'-'\246' '\248'-'\255'
+ '\'' '0'-'9' '@' ]
+
let symbolchar_symbol_no_brackets =
['!' '$' '%' '&' '*' '+' ',' '^' '#'
'\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
@@ -558,36 +639,161 @@ and doc_bol = parse
| space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
{ let eol, lex = strip_eol (lexeme lexbuf) in
let lev, s = sec_title lex in
- Output.section lev (fun () -> ignore (doc (from_string s)));
- if eol then doc_bol lexbuf else doc lexbuf }
+ if subtitle (Output.get_module false) s then
+ ()
+ else
+ Output.section lev (fun () -> ignore (doc None (from_string s)));
+ if eol then doc_bol lexbuf else doc None lexbuf }
+ | space* nl space* '-'+
+ { (* adding this production instead of just letting the paragraph
+ production and the begin list production fire eliminates
+ extra vertical whitespace. *)
+ let buf' = lexeme lexbuf in
+ let buf =
+ let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
+ match bufs with
+ | (_ :: s :: []) -> s
+ | (_ :: _ :: s :: _) -> s
+ | _ -> eprintf "Internal error bad_split1 - please report\n";
+ exit 1
+ in
+ match check_start_list buf with
+ | Neither -> backtrack_past_newline lexbuf; doc None lexbuf
+ | List n -> Output.item 1; doc (Some [n]) lexbuf
+ | Rule -> Output.rule (); doc None lexbuf
+ }
| space* '-'+
- { let n = count_dashes (lexeme lexbuf) in
- if n >= 4 then Output.rule () else Output.item n;
- doc lexbuf }
+ { let buf = lexeme lexbuf in
+ match check_start_list buf with
+ | Neither -> backtrack lexbuf; doc None lexbuf
+ | List n -> Output.item 1; doc (Some [n]) lexbuf
+ | Rule -> Output.rule (); doc None lexbuf
+ }
| "<<" space*
{ Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
| eof
{ true }
+ | '_'
+ { Output.start_emph ();
+ doc None lexbuf }
| _
- { backtrack lexbuf; doc lexbuf }
+ { backtrack lexbuf; doc None lexbuf }
+
+(*s Scanning lists - using whitespace *)
+and doc_list_bol indents = parse
+ | space* '-'
+ { let (n_spaces,_) = count_spaces (lexeme lexbuf) in
+ match find_level indents n_spaces with
+ | Before -> backtrack lexbuf; doc_bol lexbuf
+ | StartLevel n -> Output.item n; doc (Some (take n indents)) lexbuf
+ | InLevel (n,true) ->
+ let items = List.length indents in
+ Output.item (items+1);
+ doc (Some (List.append indents [n_spaces])) lexbuf
+ | InLevel (_,false) ->
+ backtrack lexbuf; doc_bol lexbuf
+ }
+ | "<<" space*
+ { Output.start_verbatim ();
+ verbatim lexbuf;
+ doc_list_bol indents lexbuf }
+ | "[[" nl
+ { formatted := true;
+ Output.paragraph ();
+ Output.start_inline_coq ();
+ ignore(body_bol lexbuf);
+ Output.end_inline_coq ();
+ formatted := false;
+ doc_list_bol indents lexbuf }
+ | space* nl space* '-'
+ { (* Like in the doc_bol production, these two productions
+ exist only to deal properly with whitespace *)
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf }
+ | space* nl space* _
+ { let buf' = lexeme lexbuf in
+ let buf =
+ let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
+ match bufs with
+ | (_ :: s :: []) -> s
+ | (_ :: _ :: s :: _) -> s
+ | _ -> eprintf "Internal error bad_split2 - please report\n";
+ exit 1
+ in
+ let (n_spaces,_) = count_spaces buf in
+ match find_level indents n_spaces with
+ | InLevel _ ->
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
+ | StartLevel n ->
+ if n = 1 then
+ begin
+ Output.stop_item ();
+ backtrack_past_newline lexbuf;
+ doc_bol lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
+ end
+ | Before -> Output.stop_item ();
+ backtrack_past_newline lexbuf;
+ doc_bol lexbuf
-(*s Scanning documentation elsewhere *)
+ }
+ | space* _
+ { let (n_spaces,_) = count_spaces (lexeme lexbuf) in
+ match find_level indents n_spaces with
+ | Before -> Output.stop_item (); backtrack lexbuf;
+ doc_bol lexbuf
+ | StartLevel n ->
+ Output.reach_item_level (n-1);
+ backtrack lexbuf;
+ doc (Some (take (n-1) indents)) lexbuf
+ | InLevel (n,_) ->
+ Output.reach_item_level n;
+ backtrack lexbuf;
+ doc (Some (take n indents)) lexbuf
+ }
-and doc = parse
+(*s Scanning documentation elsewhere *)
+and doc indents = parse
| nl
- { Output.char '\n'; doc_bol lexbuf }
+ { Output.char '\n';
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
+ | None -> doc_bol lexbuf }
| "[[" nl
{ if !Cdglobals.plain_comments
- then (Output.char '['; Output.char '['; doc lexbuf)
+ then (Output.char '['; Output.char '['; doc indents 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)}
+ if eol then
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
+ | None -> doc_bol lexbuf
+ else doc indents lexbuf)}
+ | "[]"
+ { Output.symbol "PROOFBOX"; doc indents lexbuf }
| "["
{ if !Cdglobals.plain_comments then Output.char '['
else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf;
- Output.end_inline_coq ()); doc lexbuf }
+ Output.end_inline_coq ()); doc indents lexbuf }
+ | "(*"
+ { backtrack lexbuf ;
+ let bol_parse = match indents with
+ | Some is -> doc_list_bol is
+ | None -> doc_bol
+ in
+ let eol = comment lexbuf in
+ if eol then bol_parse lexbuf else doc indents lexbuf
+ }
| '*'* "*)" space* nl
{ true }
| '*'* "*)"
@@ -595,26 +801,37 @@ and doc = parse
| "$"
{ if !Cdglobals.plain_comments then Output.char '$'
else (Output.start_latex_math (); escaped_math_latex lexbuf);
- doc lexbuf }
+ doc indents lexbuf }
| "$$"
{ if !Cdglobals.plain_comments then Output.char '$';
- Output.char '$'; doc lexbuf }
+ Output.char '$'; doc indents lexbuf }
| "%"
{ if !Cdglobals.plain_comments then Output.char '%'
- else escaped_latex lexbuf; doc lexbuf }
+ else escaped_latex lexbuf; doc indents lexbuf }
| "%%"
{ if !Cdglobals.plain_comments then Output.char '%';
- Output.char '%'; doc lexbuf }
+ Output.char '%'; doc indents lexbuf }
| "#"
{ if !Cdglobals.plain_comments then Output.char '#'
- else escaped_html lexbuf; doc lexbuf }
+ else escaped_html lexbuf; doc indents lexbuf }
| "##"
{ if !Cdglobals.plain_comments then Output.char '#';
- Output.char '#'; doc lexbuf }
+ Output.char '#'; doc indents lexbuf }
+ | nonidentchar '_' nonidentchar
+ { List.iter (fun x -> Output.char (lexeme_char lexbuf x)) [0;1;2];
+ doc indents lexbuf}
+ | nonidentchar '_'
+ { Output.char (lexeme_char lexbuf 0);
+ Output.start_emph ();
+ doc indents lexbuf }
+ | '_' nonidentchar
+ { Output.stop_emph ();
+ Output.char (lexeme_char lexbuf 1);
+ doc indents lexbuf }
| eof
{ false }
| _
- { Output.char (lexeme_char lexbuf 0); doc lexbuf }
+ { Output.char (lexeme_char lexbuf 0); doc indents lexbuf }
(*s Various escapings *)
@@ -638,7 +855,8 @@ and escaped_html = parse
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
and verbatim = parse
- | nl ">>" space* nl? { Output.verbatim_char '\n'; Output.stop_verbatim () }
+ | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
+ | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
| eof { Output.stop_verbatim () }
| _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
@@ -672,7 +890,7 @@ and comments = parse
| '"' [^ '"']* '"'
{ let s = lexeme lexbuf in
let s = String.sub s 1 (String.length s - 2) in
- ignore (doc (from_string s)); comments lexbuf }
+ ignore (doc None (from_string s)); comments lexbuf }
| ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
{ escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
| "." (space_nl | eof)
@@ -718,7 +936,7 @@ and comment = parse
{ if !Cdglobals.parse_comments
then
(if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
- doc lexbuf }
+ doc None lexbuf }
| "%"
{ if !Cdglobals.parse_comments
then
@@ -761,12 +979,46 @@ and body_bol = parse
and body = parse
| nl {Output.line_break(); body_bol lexbuf}
- | nl+ space* "]]"
- { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
+ | nl+ space* "]]" space* nl
+ { if not !formatted then
+ begin
+ symbol lexbuf (lexeme lexbuf);
+ body lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end }
+ | "]]" space* nl
+ { if not !formatted then
+ begin
+ symbol lexbuf (lexeme lexbuf);
+ body lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end }
| eof { false }
| '.' space* nl | '.' space* eof
{ Output.char '.'; Output.line_break();
if not !formatted then true else body_bol lexbuf }
+ | '.' space* nl "]]" space* nl
+ { Output.char '.';
+ if not !formatted then
+ begin
+ eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf);
+ flush stderr;
+ exit 1
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end
+ }
| '.' space+ { Output.char '.'; Output.char ' ';
if not !formatted then false else body lexbuf }
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
@@ -821,18 +1073,51 @@ and printing_token_body = parse
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
printing_token_body lexbuf }
+(*s A small scanner to support the chapter subtitle feature *)
+and st_start m = parse
+ | "(*" "*"+ space+ "*" space+
+ { st_modname m lexbuf }
+ | _
+ { None }
+
+and st_modname m = parse
+ | identifier space* ":" space*
+ { if subtitle m (lexeme lexbuf) then
+ st_subtitle lexbuf
+ else
+ None
+ }
+ | _
+ { None }
+
+and st_subtitle = parse
+ | [^ '\n']* '\n'
+ { let st = lexeme lexbuf in
+ let i = try Str.search_forward (Str.regexp "\\**)") st 0 with
+ Not_found ->
+ (eprintf "unterminated comment at beginning of file\n";
+ exit 1)
+ in
+ Some (cut_head_tail_spaces (String.sub st 0 i))
+ }
+ | _
+ { None }
(*s Applying the scanners to files *)
{
-
let coq_file f m =
reset ();
- Index.current_library := m;
- Output.start_module ();
let c = open_in f in
let lb = from_channel c in
- Output.start_coq (); coq_bol lb; Output.end_coq ();
- close_in c
+ (Index.current_library := m;
+ Output.start_module ();
+ Output.start_coq (); coq_bol lb; Output.end_coq ();
+ close_in c)
+ let detect_subtitle f m =
+ let c = open_in f in
+ let lb = from_channel c in
+ let sub = st_start m lb in
+ close_in c;
+ sub
}
-
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index f83b1212e4..62ae42c1ad 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -43,7 +43,7 @@ type index_entry =
| Ref of coq_module * string * entry_type
| Mod of coq_module * string
-let current_type = ref Library
+let current_type : entry_type ref = ref Library
let current_library = ref ""
(** refers to the file being parsed *)
@@ -200,7 +200,9 @@ let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
let type_name = function
- | Library -> "library"
+ | Library ->
+ let ln = !lib_name in
+ if ln <> "" then String.lowercase ln else "library"
| Module -> "module"
| Definition -> "definition"
| Inductive -> "inductive"
@@ -236,8 +238,8 @@ let all_entries () =
idx_entries = sort_entries !gl;
idx_size = List.length !gl },
Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
- idx_entries = sort_entries e;
- idx_size = List.length e }) :: l) bt []
+ idx_entries = sort_entries e;
+ idx_size = List.length e }) :: l) bt []
}
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 301f4bdf70..3c4c9a6566 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -46,6 +46,7 @@ let usage () =
prerr_endline " --with-footer <file> append <file> as html footer";
prerr_endline " --no-index do not output the index";
prerr_endline " --multi-index index split in multiple files";
+ prerr_endline " --index <string> set index name (default is index)";
prerr_endline " --toc output a table of contents";
prerr_endline " --vernac <file> consider <file> as a .v file";
prerr_endline " --tex <file> consider <file> as a .tex file";
@@ -67,6 +68,10 @@ let usage () =
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 " --toc-depth <int> don't include TOC entries for sections below level <int>";
+ prerr_endline " --no-lib-name don't display \"Library\" before library names in the toc";
+ prerr_endline " --lib-name <string> call top level toc entries <string> instead of \"Library\"";
+ prerr_endline " --lib-subtitles first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
prerr_endline "";
exit 1
@@ -229,6 +234,10 @@ let parse () =
index := false; parse_rec rem
| ("-multi-index" | "--multi-index") :: rem ->
multi_index := true; parse_rec rem
+ | ("-index" | "--index") :: s :: rem ->
+ Cdglobals.index_name := s; parse_rec rem
+ | ("-index" | "--index") :: [] ->
+ usage ()
| ("-toc" | "--toc" | "--table-of-contents") :: rem ->
toc := true; parse_rec rem
| ("-stdout" | "--stdout") :: rem ->
@@ -281,6 +290,25 @@ let parse () =
Cdglobals.plain_comments := true; parse_rec rem
| ("-interpolate" | "--interpolate") :: rem ->
Cdglobals.interpolate := true; parse_rec rem
+ | ("-toc-depth" | "--toc-depth") :: [] ->
+ usage ()
+ | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
+ let d = try int_of_string ds with
+ Failure _ ->
+ (eprintf "--toc-depth must be followed by an integer";
+ exit 1)
+ in
+ Cdglobals.toc_depth := Some d;
+ parse_rec rem
+ | ("-no-lib-name" | "--no-lib-name") :: rem ->
+ Cdglobals.lib_name := "";
+ parse_rec rem
+ | ("-lib-name" | "--lib-name") :: ds :: rem ->
+ Cdglobals.lib_name := ds;
+ parse_rec rem
+ | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
+ Cdglobals.lib_subtitles := true;
+ parse_rec rem
| ("-latin1" | "--latin1") :: rem ->
Cdglobals.set_latin1 (); parse_rec rem
@@ -386,7 +414,9 @@ let copy src dst =
let gen_one_file l =
let file = function
| Vernac_file (f,m) ->
- Output.set_module m; Cpretty.coq_file f m
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
+ Output.set_module m sub;
+ Cpretty.coq_file f m
| Latex_file _ -> ()
in
if (!header_trailer) then Output.header ();
@@ -398,8 +428,9 @@ let gen_one_file l =
let gen_mult_files l =
let file = function
| Vernac_file (f,m) ->
- Output.set_module m;
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
let hf = target_full_name m in
+ Output.set_module m sub;
open_out_file hf;
if (!header_trailer) then Output.header ();
Cpretty.coq_file f m;
@@ -410,7 +441,7 @@ let gen_mult_files l =
List.iter file l;
if (!index && !target_language=HTML) then begin
if (!multi_index) then Output.make_multi_index ();
- open_out_file "index.html";
+ open_out_file (!index_name^".html");
page_title := (if !title <> "" then !title else "Index");
if (!header_trailer) then Output.header ();
Output.make_index ();
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index b69e8b3695..2d2a86ef0e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -77,13 +77,24 @@ let is_tactic =
(*s Current Coq module *)
-let current_module = ref ""
+let current_module : (string * string option) ref = ref ("",None)
-let set_module m = current_module := m; page_title := m
+let get_module withsub =
+ let (m,sub) = !current_module in
+ if withsub then
+ match sub with
+ | None -> m
+ | Some sub -> m ^ ": " ^ sub
+ else
+ m
+
+let set_module m sub = current_module := (m,sub);
+ page_title := get_module true
(*s Common to both LaTeX and HTML *)
let item_level = ref 0
+let in_doc = ref false
(*s Customized pretty-print *)
@@ -119,14 +130,15 @@ let initialize () =
"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
- "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"
+ "λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
+ "PROOFBOX", "\\ensuremath{\\Box}", Some "<font size=-2>&#9744;</font>"; (* FIX THIS *)
(* "fun", "\\ensuremath{\\lambda}" ? *)
]
(*s Table of contents *)
type toc_entry =
- | Toc_library of string
+ | Toc_library of string * string option
| Toc_section of int * (unit -> unit) * string
let (toc_q : toc_entry Queue.t) = Queue.create ()
@@ -140,7 +152,6 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
module Latex = struct
let in_title = ref false
- let in_doc = ref false
(*s Latex preamble *)
@@ -155,6 +166,10 @@ module Latex = struct
printf "\\usepackage[T1]{fontenc}\n";
printf "\\usepackage{fullpage}\n";
printf "\\usepackage{coqdoc}\n";
+ printf "\\usepackage{amsmath,amssymb}\n";
+ match !toc_depth with
+ | None -> ()
+ | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n;
Queue.iter (fun s -> printf "%s\n" s) preamble;
printf "\\begin{document}\n"
end;
@@ -202,12 +217,15 @@ module Latex = struct
for i = 0 to String.length s - 1 do label_char s.[i] done
let start_module () =
- if not !short then begin
- printf "\\coqlibrary{";
- label_ident !current_module;
- printf "}{";
- raw_ident !current_module;
- printf "}\n\n"
+ let ln = !lib_name in
+ if not !short then begin
+ printf "\\coqlibrary{";
+ label_ident (get_module false);
+ printf "}{";
+ if ln <> "" then printf "%s " ln;
+ printf "}{";
+ raw_ident (get_module true);
+ printf "}\n\n"
end
let start_latex_math () = output_char '$'
@@ -262,7 +280,7 @@ module Latex = struct
let reference s = function
| Def (fullid,typ) ->
- defref !current_module fullid typ s
+ defref (get_module false) fullid typ s
| Mod (m,s') when s = s' ->
module_ref m s
| Ref (m,fullid,typ) ->
@@ -276,14 +294,14 @@ module Latex = struct
end else begin
begin
try
- reference s (Index.find !current_module loc)
+ reference s (Index.find (get_module false) loc)
with Not_found ->
if is_tactic s then begin
printf "\\coqdoctac{"; raw_ident s; printf "}"
end else begin
if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
then
- try reference s (Index.find_string !current_module s)
+ try reference s (Index.find_string (get_module false) s)
with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
else (printf "\\coqdocvar{"; raw_ident s; printf "}")
end
@@ -322,6 +340,12 @@ module Latex = struct
let comment c = char c
+ (* This is broken if we are in math mode, but coqdoc currently isn't
+ tracking that *)
+ let start_emph () = printf "\\textit{ "
+
+ let stop_emph () = printf "}"
+
let start_comment () = printf "\\begin{coqdoccomment}\n"
let end_comment () = printf "\\end{coqdoccomment}\n"
@@ -350,7 +374,7 @@ module Latex = struct
let rule () =
printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
- let paragraph () = stop_item (); printf "\n\n"
+ let paragraph () = printf "\n\n"
let line_break () = printf "\\coqdoceol\n"
@@ -372,7 +396,7 @@ end
(*s HTML output *)
module Html = struct
-
+
let header () =
if !header_trailer then
if !header_file_spec then
@@ -396,8 +420,8 @@ module Html = struct
end
let trailer () =
- if !index && !current_module <> "Index" then
- printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
+ if !index && (get_module false) <> "Index" then
+ printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
if !header_trailer then
if !footer_file_spec then
let cin = Pervasives.open_in !footer_file in
@@ -415,9 +439,14 @@ module Html = struct
end
let start_module () =
+ let ln = !lib_name in
if not !short then begin
- add_toc_entry (Toc_library !current_module);
- printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
+ let (m,sub) = !current_module in
+ add_toc_entry (Toc_library (m,sub));
+ if ln = "" then
+ printf "<h1 class=\"libtitle\">%s</h1>\n\n" (get_module true)
+ else
+ printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true)
end
let indentation n = for i = 1 to n do printf "&nbsp;" done
@@ -472,6 +501,19 @@ module Html = struct
| Coqlib | Unknown ->
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
+ let reference s r =
+ match r with
+ | Def (fullid,ty) ->
+ printf "<a name=\"%s\">" fullid;
+ printf "<span class=\"id\" type=\"%s\">" (type_name ty);
+ raw_ident s; printf "</span></a>"
+ | Mod (m,s') when s = s' ->
+ module_ref m s
+ | Ref (m,fullid,ty) ->
+ ident_ref m fullid (type_name ty) s
+ | Mod _ ->
+ printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>"
+
let ident s loc =
if is_keyword s then begin
printf "<span class=\"id\" type=\"keyword\">";
@@ -479,25 +521,19 @@ module Html = struct
printf "</span>"
end else
begin
- 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);
- raw_ident s; printf "</span></a>"
- | Mod (m,s') when s = s' ->
- module_ref m s
- | Ref (m,fullid,ty) ->
- ident_ref m fullid (type_name ty) s
- | Mod _ ->
- printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
- with Not_found ->
- if is_tactic s then
- (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
- else
- (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
+ try reference s (Index.find (get_module false) loc)
+ with Not_found ->
+ if is_tactic s then
+ (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
+ else
+ if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+ then
+ try reference s (Index.find_string (get_module false) s)
+ with _ ->
+ (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
+ else (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
end
-
+
let with_html_printing f tok =
try
(match Hashtbl.find token_pp tok with
@@ -514,7 +550,7 @@ module Html = struct
let rec reach_item_level n =
if !item_level < n then begin
- printf "\n<ul>\n<li>"; incr item_level;
+ printf "<ul>\n<li>"; incr item_level;
reach_item_level n
end else if !item_level > n then begin
printf "\n</li>\n</ul>\n"; decr item_level;
@@ -532,14 +568,18 @@ module Html = struct
let end_coq () = if not !raw_comments then printf "</div>\n"
- let start_doc () =
+ let start_doc () = in_doc := true;
if not !raw_comments then
printf "\n<div class=\"doc\">\n"
- let end_doc () =
+ let end_doc () = in_doc := false;
stop_item ();
if not !raw_comments then printf "\n</div>\n"
+ let start_emph () = printf "<i>"
+
+ let stop_emph () = printf "</i>"
+
let start_comment () = printf "<span class=\"comment\">(*"
let end_comment () = printf "*)</span>"
@@ -552,16 +592,15 @@ module Html = struct
let end_inline_coq () = printf "</span>"
- let paragraph () =
- let i = !item_level in
- stop_item ();
- if i > 0 then printf "\n"
- else printf "\n<br/> <br/>\n"
+ let paragraph () = printf "\n<br/> <br/>\n"
let section lev f =
let lab = new_label () in
- let r = sprintf "%s.html#%s" !current_module lab in
- add_toc_entry (Toc_section (lev, f, r));
+ let r = sprintf "%s.html#%s" (get_module false) lab in
+ match !toc_depth with
+ | None -> add_toc_entry (Toc_section (lev, f, r))
+ | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r))
+ else ();
stop_item ();
printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
f ();
@@ -572,7 +611,7 @@ module Html = struct
(* make a HTML index from a list of triples (name,text,link) *)
let index_ref i c =
let idxc = sprintf "%s_%c" i.idx_name c in
- if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc
+ !index_name ^ (if !multi_index then "_" ^ idxc ^ ".html" else ".html#" ^ idxc)
let letter_index category idx (c,l) =
if l <> [] then begin
@@ -591,8 +630,12 @@ module Html = struct
let format_global_index =
Index.map
(fun s (m,t) ->
- if t = Library then
- "[library]", m ^ ".html"
+ if t = Library then
+ let ln = !lib_name in
+ if ln <> "" then
+ "[" ^ String.lowercase ln ^ "]", m ^ ".html"
+ else
+ "[library]", m ^ ".html"
else
sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
sprintf "%s.html#%s" m s)
@@ -629,7 +672,7 @@ module Html = struct
(* Attn: make_one_multi_index créé un nouveau fichier... *)
let idx = i.idx_name in
let one_letter ((c,l) as cl) =
- open_out_file (sprintf "index_%s_%c.html" idx c);
+ open_out_file (sprintf "%s_%s_%c.html" !index_name idx c);
if (!header_trailer) then header ();
prt_tbl (); printf "<hr/>";
letter_index true idx cl;
@@ -659,7 +702,7 @@ module Html = struct
all_letters i
end
in
- current_module := "Index";
+ set_module "Index" None;
if !title <> "" then printf "<h1>%s</h1>\n" !title;
print_table ();
if not (!multi_index) then
@@ -668,21 +711,25 @@ module Html = struct
printf "<hr/>"; print_table ()
end
-
- 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) ->
- 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 ();
-
+ let make_toc () =
+ let ln = !lib_name in
+ let make_toc_entry = function
+ | Toc_library (m,sub) ->
+ stop_item ();
+ let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
+ if ln = "" then
+ printf "<a href=\"%s.html\"><h2>%s</h2></a>\n" m ms
+ else
+ printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms
+ | Toc_section (n, f, r) ->
+ item n;
+ printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+ in
+ printf "<div id=\"toc\">\n";
+ Queue.iter make_toc_entry toc_q;
+ stop_item ();
+ printf "</div>\n"
+
end
@@ -692,8 +739,6 @@ module TeXmacs = struct
(*s Latex preamble *)
- let in_doc = ref false
-
let (preamble : string Queue.t) =
in_doc := false; Queue.create ()
@@ -789,6 +834,9 @@ module TeXmacs = struct
let end_coq () = ()
+ let start_emph () = printf "<with|font shape|italic|"
+ let stop_emph () = printf ">"
+
let start_comment () = ()
let end_comment () = ()
@@ -810,7 +858,7 @@ module TeXmacs = struct
let rule () =
printf "\n<hrule>\n"
- let paragraph () = stop_item (); printf "\n\n"
+ let paragraph () = printf "\n\n"
let line_break_true () = printf "<format|line break>"
@@ -874,14 +922,17 @@ module Raw = struct
let symbol s = raw_ident s
let item n = printf "- "
-
let stop_item () = ()
+ let reach_item_level _ = ()
let start_doc () = printf "(** "
let end_doc () = printf " *)\n"
- let start_comment () = ()
- let end_comment () = ()
+ let start_emph () = printf "_"
+ let stop_emph () = printf "_"
+
+ let start_comment () = printf "(*"
+ let end_comment () = printf "*)"
let start_coq () = ()
let end_coq () = ()
@@ -891,10 +942,10 @@ module Raw = struct
let section_kind =
function
- | 1 -> "*"
- | 2 -> "**"
- | 3 -> "***"
- | 4 -> "****"
+ | 1 -> "* "
+ | 2 -> "** "
+ | 3 -> "*** "
+ | 4 -> "**** "
| _ -> assert false
let section lev f =
@@ -959,6 +1010,7 @@ let empty_line_of_code = select
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 reach_item_level = select Latex.reach_item_level Html.reach_item_level TeXmacs.reach_item_level Raw.reach_item_level
let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
let char = select Latex.char Html.char TeXmacs.char Raw.char
@@ -972,6 +1024,11 @@ let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html
let html_string =
select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
+let start_emph =
+ select Latex.start_emph Html.start_emph TeXmacs.start_emph Raw.start_emph
+let stop_emph =
+ select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph
+
let start_latex_math =
select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
let stop_latex_math =
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 181ccf1cab..6e3f6e88b0 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -16,7 +16,8 @@ val initialize : unit -> unit
val add_printing_token : string -> string option * string option -> unit
val remove_printing_token : string -> unit
-val set_module : coq_module -> unit
+val set_module : coq_module -> string option -> unit
+val get_module : bool -> string
val header : unit -> unit
val trailer : unit -> unit
@@ -28,6 +29,9 @@ val start_module : unit -> unit
val start_doc : unit -> unit
val end_doc : unit -> unit
+val start_emph : unit -> unit
+val stop_emph : unit -> unit
+
val start_comment : unit -> unit
val end_comment : unit -> unit
@@ -48,6 +52,8 @@ val empty_line_of_code : unit -> unit
val section : int -> (unit -> unit) -> unit
val item : int -> unit
+val stop_item : unit -> unit
+val reach_item_level : int -> unit
val rule : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 02:34:24 +0000