Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,

M. Greenberg) and add support for interpolation to HTML output. The
patch is mostly backwards-compatible, except for the CSS style which
needs more readaptation. Doc for the new options will come as well.
 
- lists have been updated substantially.  In particular,
 multiparagraph list items are now supported and sublists work
 better, using an "off-side" rule.

- the "--index" flag allows one to change the name of the generated
 index file (good since index.html has a special meaning).

- the "--toc-depth <int>" flag allows one to limit how many levels are
 included in the toc.

- the "--lib-name <string>" flag allows one to specify what libraries
 are called, instead of just sticking "Library" before each module
 name (for example, "Module" or "Chapter" might be more sensible in
 some contexts).  Additionally "--no-lib-name" eliminates this extra
 title completely.

- the "--lib-subtitles" flag allows one to specify subtitles for
 libraries.  When enabled, the beginning of each file is checked
 for a comment of the form:

(** * ModuleName : text *)

 and the text will be printed as a subtitle in the appropriate
 places.

- Text can be made italic by putting it inside underscores, as in:
 _emphasized text_.  This has the advantage of looking OK in the
 .v file as well.  A few simple rules are followed to make sure
 identifiers with underscores aren't accidentally made italic.

- Various changes have been made in an attempt to beautify the output,
 especially in html, while allowing the .v sources to look decent as
 well.  Mostly these involve whitespace.

- The coqdoc.css file has been changed.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12308 85f007b7-540e-0410-9357-904b9bb8a0f7

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