| Age | Commit message (Collapse) | Author |
|---|
|
This does not affect the rendering but gives better structured
html/tex files.
|
|
We clarify that there are two kinds of verbatim: inline and block.
We add a test testing verbatim and others.
Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
|
|
The line count remains fragile though... Any idea to do it
automatically?
|
|
The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.
|
|
Fix #12742
|
|
Reviewed-by: Zimmi48
|
|
|
|
starting emphasis.
This is to support referring to names such as _CoqProject.
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
|
|
Fixes BZ#5700
|
|
|
|
|
|
Moreover, this commit makes sure that an empty line after a list is always
translated into a break. ("StartLevel 1" was excluded, for some reason.)
It also avoids some code duplication. In particular, "stop_item ()" is
defined as "reach_item_level 0", so there is no reason to handle
"StartLevel 1" specially.
|
|
|
|
#4770).
This also fixes comments not being properly skipped when looking for eol.
|
|
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#3802.)
|
|
|
|
Just like the [Record] keyword allows only non-recursive records.
|
|
|
|
locations found when parsing expressions in comments and the absolute
locations in the glob file).
As now, the glob file does not parse comment, so I removed the test
for location when parsing expressions in comments, which anyway are
not linkable, precisely because not parsed by coqc.
|
|
|
|
Anyway, a few syntactic features of 3.12 were already used here and
there (e.g. local opening via Foo.(...), or the record shortcut
{ field; ... }). Hence compiling with 3.11 wasn't working anymore.
Already take advantage of the following 3.12.1 features :
- "module type of ..." in CArray, CList, CString ...
- "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
via our coqdep to localize the .ml4 modules :-)
The -ml-synonym option (+ various bugfixes) is the reason for asking
3.12.1 directly and not just 3.12.0. After all, if debian stable is
providing 3.12.1, then everybody has it ;-)
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Patch by Adam Chilipala.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
markup/typesetting to coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(bug apparently introduced by r11880).
Fixing also a "body_bol" which apparently should be a "bol".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
without knowing it.
Note: location tables have grown a lot, a better representation of the
contents of the glob files in coqdoc might improve efficiency.
Also added keywords.
Information is now obtained from the glob file to know the exact span
of identifiers. Kept a class of identifiers (and enriched them) for
the main purpose of distinguishing between idents and symbols in the
absence of a glob file.
Still a lot of work to do in coqdoc to make it more robust...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14482 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
symbol).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- single quotes in notations were breaking coqdoc, even raising an
out-of-bound error when appearing in the last character of the notation;
- letter "x" in notation tokens were inelegantly surrounded by single quotes,
- rare, but allowed characters < 32 were lost in index pages.
A new fully injective space-free-and-human-readable encoding algorithm
is adopted which put single quotes around all terminal tokens,
double existing single quotes, and replace invisible characters by
^X-like strings.
Moreover, the keywords "Local"/"Global" were blocking the detection of
keywords starting coq lines (e.g. "Local Notation" was not recognized
as a notation). "Local" and "Global" are now uniformly treated as
modifiers of vernac commands as they are in the Coq parser.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
this lacks robustness since "coqdoc -g" will drop away any commands unknown
from coqdoc, leading to possible synchronisation problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
These declarations (e.g. make -C .. bin/coqtop.byte) are quite
annoying when debugging stuff over the whole archive: all of a
sudden, M-x recompile isn't doing what you intended just because
you've visited some specific files. Instead:
- Feel free to rather add intermediate targets in the Makefile if
they aren't there yet.
- For avoiding typing the -C with many .. after, you can have a
look at my recursively-descending make:
http://www.pps.jussieu.fr/~letouzey/download/make.sh
which is to be renamed make and placed in a bin dir with more
priority than /usr/bin. Beware! I've already add a few bad surprises
with this hack, but it's really convenient nonetheless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
