From 49114c2ec22d8a238a1e939dbc233da7e99d59cb Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 28 Sep 2010 18:53:05 +0000 Subject: 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 --- tools/coqdoc/main.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'tools/coqdoc/main.ml') 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 insert in LaTeX preamble"; prerr_endline " --files-from read file names to process in "; prerr_endline " --glob-from read globalization information from "; + 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 call top level toc entries 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 -> -- cgit v1.2.3