diff options
| author | msozeau | 2009-09-10 21:54:37 +0000 |
|---|---|---|
| committer | msozeau | 2009-09-10 21:54:37 +0000 |
| commit | 809c9dd5a2f0bedbbd3ef55809748dd1a56837f0 (patch) | |
| tree | 390fe5a92862ca45ea3da923c1d2b1e2b5132f88 /tools | |
| parent | d7609a04877b54dbf019cfd51abedacb955f1b20 (diff) | |
Fixes for toc depth handling and handling of substitles from Chris Casinghino.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12318 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 3 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 14 |
2 files changed, 9 insertions, 8 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 065b72e7b3..d9ed862972 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -639,7 +639,8 @@ 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 - if subtitle (Output.get_module false) s then + if (!Cdglobals.lib_subtitles) && + (subtitle (Output.get_module false) s) then () else Output.section lev (fun () -> ignore (doc None (from_string s))); diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index b2e6bbd992..302cbffce8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -166,9 +166,9 @@ module Latex = struct 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; + (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; @@ -600,10 +600,10 @@ module Html = struct let section lev f = let lab = new_label () in 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 (); + (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 (); |