Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces the

ability to format inference rules (delimited by [[[ ]]]) and adds some
new flags. Here's the message from Chris:

- coqdoc now has support for inference rules inside coqdoc comments.
 These should be enclosed in triple square brackets with the
 following format.

[[[
                      |- t1 : Bool
                 |- t2 : T    |- t3 : T
               ----------------------------                   (T_If)
               |- if t1 then t2 else t3 : T
]]]

 The rule's name is optional.  Multiple inference rules may be
 included in the same [[[ ]]] block, separated by blank lines.
 See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469
 for some examples of the output.  The output will only be pretty
 in html - in other formats it is printed verbatim (though it
 shouldn't be hard to add latex support, and I may soon).

- Two new coqdoc flags have been added.  First, --inline-notmono
 causes inline code to be printed in a proportional width font
 (adjustable in the css file).  Second, --no-glob tells coqdoc not to
 look for .glob files (no links will be inserted for identifiers when
 this flag is used).

- Finally, the handling of paragraphs and whitespace around lists
 has been made somewhat saner.


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

6 files changed, 250 insertions, 37 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index cfe86a276..1b1a321e6 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -74,6 +74,7 @@ let toc_depth = (ref None : int option ref)
 let lib_name = ref "Library"
 let lib_subtitles = ref false
 let interpolate = ref false
+let inline_notmono = ref false
 
 let charset = ref "iso-8859-1"
 let inputenc = ref ""
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 24b514b76..ccd285f18 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -101,8 +101,13 @@ h4.section {
     color: rgb(30%,30%,70%);
     font-family: monospace } 
 
-.doc .inlinecode .id {
-    color: rgb(30%,30%,70%);
+.doc .inlinecode .id { 
+    color: rgb(30%,30%,70%); 
+} 
+
+.inlinecodenm { 
+    display: inline;
+    color: #444444;
 }
 
 .doc .code { 
@@ -124,6 +129,32 @@ h4.section {
     font-family: monospace;
  } 
 
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: monospace;
+    text-align: center;
+/*    color: rgb(35%,35%,70%);  */
+    padding: 0px;
+    line-height: 100%;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%); 
+    font-size: 80%;
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
 /* Pied de page */
 
 #footer { font-size: 65%;
@@ -231,4 +262,13 @@ h4.section {
     position: absolute;
     bottom: 0;
     text-align: bottom;
-}
\ No newline at end of file
+}
+
+.paragraph {
+    height: 0.75em;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index c018e66e3..8fb705f2c 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -648,8 +648,6 @@ and coq = parse
 (*s Scanning documentation, at beginning of line *)
 
 and doc_bol = parse
-  | space* nl+
-      { Output.paragraph (); doc_bol lexbuf }
   | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
       { let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
@@ -659,31 +657,24 @@ and doc_bol = parse
           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
+  | space_nl* '-'+
+      { let buf' = lexeme lexbuf in
+        let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
+        let lines = (List.length bufs) - 1 in
+        let line = 
+          match bufs with
+          | [] -> eprintf "Internal error bad_split1 - please report\n";
+                  exit 1
+          | _ -> List.nth bufs lines
         in
-          match check_start_list buf with
+          match check_start_list line 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 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
+          | List n -> Output.paragraph ();
+                      Output.item 1; doc (Some [n]) lexbuf
           | Rule -> Output.rule (); doc None lexbuf
       }
+  | space* nl+
+      { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
       { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof
@@ -719,6 +710,8 @@ and doc_list_bol indents = parse
         Output.end_inline_coq_block ();
         formatted := false;
         doc_list_bol indents lexbuf }
+  | "[[[" nl
+      { inf_rules (Some indents) lexbuf }
   | space* nl space* '-'
       { (* Like in the doc_bol production, these two productions
            exist only to deal properly with whitespace *)
@@ -754,9 +747,16 @@ and doc_list_bol indents = parse
                 backtrack_past_newline lexbuf;
                 doc_list_bol indents lexbuf
               end
-        | Before -> Output.stop_item ();
-                    backtrack_past_newline lexbuf;
-                    doc_bol lexbuf
+        | Before -> 
+        (* Here we were at the beginning of a line, and it was blank.
+           The next line started before any list items.  So: insert
+           a paragraph for the empty line, rewind to whatever's just
+           after the newline, then toss over to doc_bol for whatever
+           comes next. *)
+            Output.stop_item ();
+            Output.paragraph ();
+            backtrack_past_newline lexbuf;
+            doc_bol lexbuf
 
       }
   | space* _
@@ -765,7 +765,10 @@ and doc_list_bol indents = parse
         | Before -> Output.stop_item (); backtrack lexbuf;
                     doc_bol lexbuf
         | StartLevel n ->
-            Output.reach_item_level (n-1);
+            (if n = 1 then
+               Output.stop_item ()
+             else
+               Output.reach_item_level (n-1));
             backtrack lexbuf;
             doc (Some (take (n-1) indents)) lexbuf
         | InLevel (n,_) ->
@@ -793,6 +796,8 @@ and doc indents = parse
 		  | Some ls -> doc_list_bol ls lexbuf
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
+  | "[[[" nl
+      { inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
   | "["
@@ -808,6 +813,18 @@ and doc indents = parse
         let eol = comment lexbuf in
           if eol then bol_parse lexbuf else doc indents lexbuf
       }
+  | '*'* "*)" space_nl* "(**"
+      {(match indents with
+        | Some _ -> Output.stop_item ()
+        | None -> ());
+       (* this says - if there is a blank line between the two comments,
+          insert one in the output too *)
+       let lines = List.length (Str.split_delim (Str.regexp "['\n']") 
+                                                (lexeme lexbuf))
+       in 
+         if lines > 2 then Output.paragraph ();
+       doc_bol lexbuf
+      }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
@@ -894,10 +911,16 @@ and escaped_coq = parse
       { Tokens.flush_sublexer () }
   | (identifier '.')* identifier
       { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
-  | space
-      { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
-        escaped_coq lexbuf }
-  | _
+  | space_nl*
+      { let str = lexeme lexbuf in
+          Tokens.flush_sublexer();
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.end_inline_coq ()); 
+          String.iter Output.char str; 
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.start_inline_coq ());
+          escaped_coq lexbuf }
+  | _ 
       { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
         escaped_coq lexbuf }
 
@@ -1124,6 +1147,71 @@ and printing_token_body = parse
   | _   { Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
+(*s These handle inference rules, parsing the body segments of things
+    enclosed in [[[  ]]] brackets *)
+and inf_rules indents = parse
+  | space* nl     (* blank line, before or between definitions *)
+      { inf_rules indents lexbuf }
+  | "]]]" nl      (* end of the inference rules block *)
+      { match indents with
+        | Some ls -> doc_list_bol ls lexbuf
+        | None -> doc_bol lexbuf }
+  | _ 
+      { backtrack lexbuf;  (* anything else must be the first line in a rule *)
+        inf_rules_assumptions indents [] lexbuf}
+
+(* The inference rule parsing just collects the inference rule and then
+   calls the output function once, instead of doing things incrementally
+   like the rest of the lexer.  If only there were a real parsing phase...
+*)
+and inf_rules_assumptions indents assumptions = parse
+  | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let dashes_and_name = 
+               cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
+        in
+        let ldn = String.length dashes_and_name in
+        let (dashes,name) = 
+          try (let i = String.index dashes_and_name ' ' in
+               let d = String.sub dashes_and_name 0 i in
+               let n = cut_head_tail_spaces 
+                        (String.sub dashes_and_name (i+1) (ldn-i-1))
+               in
+                 (d, Some n))
+          with _ -> (dashes_and_name, None)
+            
+        in
+          inf_rules_conclusion indents (List.rev assumptions) 
+                               (spaces, dashes, name) [] lexbuf }
+  | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let assumption = cut_head_tail_spaces 
+                            (String.sub line 0 (String.length line - 1))
+        in
+          inf_rules_assumptions indents ((spaces,assumption)::assumptions)
+                                lexbuf }
+
+(*s The conclusion is required to come immediately after the
+    horizontal bar.  It is allowed to contain multiple lines of
+    text, like the assumptions.  The conclusion ends when we spot a
+    blank line or a ']]]'. *)
+and inf_rules_conclusion indents assumptions middle conclusions = parse
+  | space* nl | space* "]]]" nl (* end of conclusions. *)
+      { backtrack lexbuf;
+        Output.inf_rule assumptions middle (List.rev conclusions);
+        inf_rules indents lexbuf }
+  | space* [^ '\n']+ nl (* this is a line in the conclusion *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let conc = cut_head_tail_spaces (String.sub line 0 
+                                                    (String.length line - 1))
+        in
+          inf_rules_conclusion indents assumptions middle 
+                               ((spaces,conc) :: conclusions) lexbuf
+      }
+
 (*s A small scanner to support the chapter subtitle feature *)
 and st_start m = parse
   | "(*" "*"+ space+ "*" space+
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index d1769fb3c..872903e6a 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -50,6 +50,7 @@ let usage () =
   prerr_endline "  -p <string>          insert <string> in LaTeX preamble";
   prerr_endline "  --files-from <file>  read file names to process in <file>";
   prerr_endline "  --glob-from <file>   read globalization information from <file>";
+  prerr_endline "  --no-glob            don't use any globalization information (no links will be inserted at identifiers)";
   prerr_endline "  --quiet              quiet mode (default)";
   prerr_endline "  --verbose            verbose mode";
   prerr_endline "  --no-externals       no links to Coq standard library";
@@ -70,6 +71,7 @@ let usage () =
   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 "  --inline-notmono     use a proportional width font for inline code (possibly with a different color)";
   prerr_endline "";
   exit 1
 
@@ -300,6 +302,9 @@ let parse () =
     | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
       Cdglobals.lib_subtitles := true;
       parse_rec rem
+    | ("-inline-notmono" | "--inline-notmono") :: rem ->
+      Cdglobals.inline_notmono := true;
+      parse_rec rem
 
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
@@ -338,6 +343,8 @@ let parse () =
 	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
+    | ("-no-glob" | "--no-glob") :: rem ->
+	glob_source := NoGlob; parse_rec rem
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
 	Cdglobals.externals := false; parse_rec rem
     | ("--external" | "-external") :: u :: logicalpath :: rem ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 938ecfb63..76c20fb02 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -627,7 +627,7 @@ module Html = struct
 
   let rec reach_item_level n =
     if !item_level < n then begin
-      printf "<ul>\n<li>"; incr item_level;
+      printf "<ul class=\"doclist\">\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;
@@ -665,7 +665,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<span class=\"inlinecode\">"
+  let start_inline_coq () = 
+    if !inline_notmono then printf "<span class=\"inlinecodenm\">"
+                       else printf "<span class=\"inlinecode\">"
 
   let end_inline_coq () = printf "</span>"
 
@@ -673,7 +675,50 @@ module Html = struct
 
   let end_inline_coq_block () = end_inline_coq ()
 
-  let paragraph () = printf "\n<br/> <br/>\n"
+  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" 
+
+  (* inference rules *)
+  let inf_rule assumptions (_,_,midnm) conclusions =
+    (* this first function replaces any occurance of 3 or more spaces
+       in a row with "&nbsp;"s.  We do this to the assumptions so that
+       people can put multiple rules on a line with nice formatting *)
+    let replace_spaces str =
+      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in 
+      let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
+      let strs = List.map (fun r -> match r with
+                                    | Str.Text s  -> [s]
+                                    | Str.Delim s -> 
+                                        copy "&nbsp;" (String.length s))  
+                          results
+      in
+        String.concat "" (List.concat strs)
+    in
+    let start_assumption line =
+          (printf "<tr class=\"infruleassumption\">\n";
+           printf "  <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in
+    let end_assumption () =
+          (printf "  <td></td>\n";
+           printf "</td>\n") in
+    let rec print_assumptions hyps = 
+          match hyps with
+          | []                 -> start_assumption "&nbsp;&nbsp;"
+          | [(_,hyp)]          -> start_assumption hyp
+          | ((_,hyp) :: hyps') -> (start_assumption hyp;
+                                   end_assumption ();
+                                   print_assumptions hyps') in
+    printf "<center><table class=\"infrule\">\n";
+    print_assumptions assumptions;
+    printf "  <td class=\"infrulenamecol\" rowspan=\"3\">\n";
+    (match midnm with
+     | None   -> printf "    &nbsp;\n  </td>" 
+     | Some s -> printf "    %s &nbsp;\n  </td>" s);
+    printf "</tr>\n";
+    printf "<tr class=\"infrulemiddle\">\n";
+    printf "  <td class=\"infrule\"><hr /></td>\n";
+    printf "</tr>\n";
+    print_assumptions conclusions;
+    end_assumption ();
+    printf "</table></center>"
 
   let section lev f =
     let lab = new_label () in
@@ -1139,6 +1184,21 @@ let verbatim_char =
   select output_char Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
+  start_verbatim ();
+  let dumb_line = 
+       function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
+                            char '\n')
+  in 
+    (List.iter dumb_line assumptions;
+     dumb_line (midsp, midln ^ (match midnm with 
+                                | Some s -> " " ^ s 
+                                | None -> ""));
+     List.iter dumb_line conclusions);
+  stop_verbatim ()
+
+let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
+
 let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
 let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
 let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index abff3df70..53d886668 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -78,6 +78,23 @@ val stop_latex_math : unit -> unit
 val start_verbatim : unit -> unit
 val stop_verbatim : unit -> unit
 
+(* this outputs an inference rule in one go.  You pass it the list of
+   assumptions, then the middle line info, then the conclusion (which
+   is allowed to span multiple lines).
+
+   In each case, the int is the number of spaces before the start of
+   the line's text and the string is the text of the line with the
+   leading trailing space trimmed.  For the middle rule, you can
+   also optionally provide a name.
+
+   We need the space info so that in modes where we aren't doing
+   something smart we can just format the rule verbatim like the user did
+*)
+val inf_rule :  (int * string) list
+             -> (int * string * (string option)) 
+             -> (int * string) list
+             -> unit
+
 val make_multi_index : unit -> unit
 val make_index : unit -> unit
 val make_toc : unit -> unit