diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/output.ml | 17 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 35 |
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 |