From 809c9dd5a2f0bedbbd3ef55809748dd1a56837f0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 10 Sep 2009 21:54:37 +0000
Subject: 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
---
 tools/coqdoc/cpretty.mll |  3 ++-
 tools/coqdoc/output.ml   | 14 +++++++-------
 2 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'tools')

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 ();
-- 
cgit v1.2.3