aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqdoc
Commit message (Collapse)AuthorAge
* New model for user-driven translation of tokens in coqdocGravatar herbelin2010-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
| | | | | | | 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
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
- 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