aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/tok.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | longer use camlp4.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fix incorrect token description for bullets.Gravatar Guillaume Melquiond2016-10-05
|
* Revert "Move bullet detection from lexer to parser (bug #5102)."Gravatar Guillaume Melquiond2016-10-05
| | | | This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
* Move bullet detection from lexer to parser (bug #5102).Gravatar Guillaume Melquiond2016-10-02
| | | | | | | | | | That way, bullet detection no longer depends on a global variable indicating whether a line is starting. This causes a small change in the recognized language. Before the commit, "--++" was recognized as a bullet "--" followed by a keyword "++" when at the start of a line; now it is always recognized as a keyword "--++". This also fixes a bug in Tok.to_string as a side-effect.
* Remove lexing of ordinal notations.Gravatar Maxime Dénès2016-07-03
| | | | | This was implemented in anticipation of a part of PR#164 that we decided not to merge.
* Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Removing the METAIDENT token, as it is not used anymore.Gravatar Pierre-Marie Pédrot2016-02-24
| | | | | | METAIDENT were idents of the form $foobar, only used in quotations. Note that it removes two dollars in the Coq codebase! Guess I'm absolved for the $(...) syntax.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
|/
* Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
| | | | | | | The fix was actually elementary. The lexer comes with a function to compare parsed tokens against tokens of the parsing rules. It is enough to have this function considering an ident in a parsing rule to be equal to the corresponding string parsed as a keyword.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* Removing some generic equalities.Gravatar ppedrot2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "KEYID token makes parsing more robust in face of notations"Gravatar gareuselesinge2013-06-21
| | | | | | This reverts commit 950086cd26f83aa8896dde9dc7ef5b3d87307c56. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16599 85f007b7-540e-0410-9357-904b9bb8a0f7
* KEYID token makes parsing more robust in face of notationsGravatar gareuselesinge2013-06-19
| | | | | | | | | A notation may introduce a new keyword that masks an quasi keyword (IDENT "of" for example) used in some grammar rules. KEYID "of" acepts both "of" as an ident and "of" as a keyword. Rephrasing grammar rules with KEYID makes hence them more robust in face of user notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of r15148 in order to compile with Camlp4Gravatar pboutill2012-04-27
| | | | | | + comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
| | | | | | Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
Cf tok.ml, token isn't anymore string*string where first string encodes the kind of the token, but rather a nice sum type. Unfortunately, string*string (a.k.a Plexing.pattern) is still used in some places of Camlp5, so there's a few conversions back and forth. But the penalty should be quite low, and having nicer tokens helps in the forthcoming integration of support for camlp4 post 3.10 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 22:59:21 +0000