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

1 files changed, 7 insertions, 0 deletions

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 ->