| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
from v8.4)
- For the style of identifiers, coqdoc was using a 'type' attribute of
tag <span>. But this attribute isn't a legal attribute of tag <span>
according to the xhtml norm. Instead, I propose to use 'title' for that.
The coqdoc.css now supports both approaches.
- The names of inner links (cross references #foo) were
containing arbitrary characters (in the case of a notation string).
For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x">
Instead, when strange characters are detected, we now hash the
string via Digest, and use this hexa hash as html label.
- And some whitespace before />
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
| |
interpretation of [[ etc... inside (* *) comments when --parse-comments
is used. Add some additional fixes from B. Pierce on formatting
verbatim and the HTML Toc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12307 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
B. Pierce on coq-club).
- Output regular comments, enclosed in a span in HTML (with (* *)
delimiters) and inside a new environment in LaTeX.
- HTML output: put the span inside anchors in links, so as to keep the
same style as for definitions (customizable in the CSS).
- Better handling of Next Obligation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12004 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Set BIBINPUTS variable correctly so that we do not use any random
biblio.bib file.
- Update setoid_rewrite doc to new typeclasses syntax and fix verb ->
texttt
- Stop using less than 100% line heights in coqdoc.css
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- correct nesting of a and div (fixes bug #2022)
- use span instead of div for inline parts
- fix standard lib template missing/new links
- use -g to produce the stdlib doc (no proofs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Better handling of spaces by actually ignoring what's inside proof
scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs
[Proof t.] and [Qed]/[Save]/...).
- Provide fancy replacements for forall,/\,... etc in HTML in case the
utf8 option is on.
- Use typesetting information in HTML output and customize the CSS
accordingly. The default color scheme follows closely the one set by
Conor for Epigram; of course one can change it.
- A try at interpolating identifiers in comments if they are defined in
the same module, with a corresponding flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11361 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre Letouzey
msozeau
notin
coq