diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-06 18:55:36 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-06 18:55:36 +0000 |
| commit | 7672bf2bdb941fd487e6c4a0e7deff1143bff680 (patch) | |
| tree | 68d2aee88883fb880b3d83a4edf60ad2626f939f /test-suite/coqdoc | |
| parent | 3ace40d1b3230f34e7d6a1961eb1fc1f972f57c9 (diff) | |
New model for user-driven translation of tokens in coqdoc
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
Diffstat (limited to 'test-suite/coqdoc')
| -rw-r--r-- | test-suite/coqdoc/links.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/coqdoc/links.v b/test-suite/coqdoc/links.v index 16028fe17..581029bdd 100644 --- a/test-suite/coqdoc/links.v +++ b/test-suite/coqdoc/links.v @@ -3,7 +3,7 @@ - symbols should not be inlined in string g - links to both kinds of notations in a' should work to the right notation - with utf8 option, forall must be unicode -- spliting between symbols and ident should be correct in a' and c +- splitting between symbols and ident should be correct in a' and c - ".." should be rendered correctly *) |