summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/output.ml17
-rw-r--r--tools/coqdoc/pretty.mll35
2 files changed, 27 insertions, 25 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 28a0cd6d..2d0bc6c2 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: output.ml 10248 2007-10-23 13:02:56Z notin $ i*)
open Cdglobals
open Index
@@ -41,8 +41,11 @@ let is_keyword =
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
"Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
- "Unset"; "Variable"; "Variables";
- "Notation";
+ "Set"; "Unset"; "Variable"; "Variables";
+ "Notation"; "Reserved Notation"; "Tactic Notation";
+ "Delimit"; "Bind"; "Open"; "Scope";
+ "Boxed"; "Unboxed";
+ "Arguments";
(* Program *)
"Program Definition"; "Program Fixpoint"; "Program Lemma";
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -285,8 +288,8 @@ module Html = struct
if !index && !current_module <> "Index" then
printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
if !header_trailer then begin
- printf "<hr/><font size=\"-1\">This page has been generated by ";
- printf "<a href=\"%s\">coqdoc</a></font>\n" self;
+ printf "<hr/>This page has been generated by ";
+ printf "<a href=\"%s\">coqdoc</a>\n" self;
printf "</div>\n\n</div>\n\n</body>\n</html>"
end
@@ -420,9 +423,9 @@ module Html = struct
let r = sprintf "%s.html#%s" !current_module lab in
add_toc_entry (Toc_section (lev, f, r));
stop_item ();
- printf "<a name=\"%s\"></a><h%d>" lab lev;
+ printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
f ();
- printf "</h%d class=\"section\">\n" lev
+ printf "</h%d>\n" lev
let rule () = printf "<hr/>\n"
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 2bf615d3..e16c7979 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*)
+(*i $Id: pretty.mll 10248 2007-10-23 13:02:56Z notin $ i*)
(*s Utility functions for the scanners *)
@@ -224,7 +224,7 @@ let decl_token =
let gallina_ext =
"Module"
- | "Declare"
+ | "Declare" space+ "Module"
| "Transparent"
| "Opaque"
| "Canonical"
@@ -327,25 +327,24 @@ rule coq_bol = parse
| space* gallina_kw_to_hide
{ let s = lexeme lexbuf in
if !light && section_or_end s then begin
- skip_to_dot lexbuf;
- coq_bol lexbuf
- end else begin
- let s = lexeme lexbuf in
- let nbsp = count_spaces s in
- indentation nbsp;
- let s = String.sub s nbsp (String.length s - nbsp) in
- ident s (lexeme_start lexbuf + nbsp);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end }
+ skip_to_dot lexbuf;
+ coq_bol lexbuf
+ end else begin
+ let nbsp = count_spaces s in
+ indentation nbsp;
+ let s = String.sub s nbsp (String.length s - nbsp) in
+ ident s (lexeme_start lexbuf + nbsp);
+ let eol= body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf
+ end }
| space* gallina_kw
{ let s = lexeme lexbuf in
- let nbsp = count_spaces s in
+ let nbsp = count_spaces s in
+ let s = String.sub s nbsp (String.length s - nbsp) in
indentation nbsp;
- let s = String.sub s nbsp (String.length s - nbsp) in
- ident s (lexeme_start lexbuf + nbsp);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
+ ident s (lexeme_start lexbuf + nbsp);
+ let eol= body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
| space* "(**" space+ "printing" space+ (identifier | token) space+
{ let tok = lexeme lexbuf in
let s = printing_token lexbuf in