| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
rules (bug report #2293).
Restored the sequential extension of the printing rules tables (that
commit #12905 replaced by a per-file modification of the printing
rules table). Note however that the table grows in the order of
compilation of files by coqdoc, which does not necessarily coincide
with the order of coqc compilation dependencies of the files.
Added documentation of coqdoc option "--external".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In the initial model (formerly to r11432), coqdoc parsed separatedly
letters and symbolic characters and was thus not able to translate
tokens mixing letters and symbolic characters such as "\in" or "=_h".
Revision 11432 extended the definition of translatable tokens by
supporting letters in it with the benefit of supporting "\in" or "=_h"
but added the constraint of requiring spaces to correctly separate
tokens in expressions such as "x : nat" which otherwise would be split
into "x" and ":nat", then leading to fail understanding "nat" as a
proper reference.
The new model renounces to define a lexical category of tokens and
uses instead a dynamically extensible sublexer similar to the one used
in the Coq lexer. The new model works even if tokens are not separated
by spaces in the source file and it thus solves problems such as the
one mentioned in bug #2273 (failure to link C in "`(!C)"). However, it
imposes a stronger discipline in writing the lexing rules in
cpretty.mll because the characters that can eventually contribute to
the application of a printing rule are buffered in the sublexer and no
output is allowed to occur until the buffer of the sublexer if
flushed.
The theoretical overhead due to the intermediate use of buffers is
apparently less than 5%. More details on the token cutting discipline
can be found in the new file token.mli.
Incidentally fixed two small problems with notation links in LaTeX:
made escaping of characters in LaTeX labels more robust so that
notations do not easily get the same label name; avoid only
highlighting the first '"' of a notation def (failing to have now a
better highlighting strategy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
In coqdoc, made links to utf8 notations working and made
representation of locations for notations more compact
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
(it interfered badly with utf-8: just take an utf-8 like "forall" which
starts in iso-8859-1 with a "a circonflex"; nothing is lost since
intentedly iso-8859-1 chars can only occur in comments and there is no
ident detection in comments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- Local Definitions were considered Global Definitions in globalization file
(bug #2288) [I made them "var" which makes them indexed like
Variables, should we have an extra category just for Let's?]
- the syntax of "[[" was not properly enforced in parse-comments mode
- improved documentation of a few vernac file of the library
- fixed a bug in Makefile.doc leading to build a bigger and bigger
Library.pdf file
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
from a incorrect computation of logical names + bug in rendering of
name-based notations, aka abbreviations or syntactic definitions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
avoiding the introduction of eta-redexes. Prioritize hints over intros
in typeclass resolution to profit from that.
Add a minor fix in coqdoc by F. Garillot.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
versions de OCaml antérieures à 3.11.0)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12512 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Théo Zimmermann
Tej Chajed
Pierre-Marie Pédrot
Guillaume Melquiond
Maxime Dénès
Hugo Herbelin
Arnaud Spiwack
Pierre Letouzey
letouzey
herbelin
pboutill
msozeau
thery
notin