aboutsummaryrefslogtreecommitdiff
path: root/parsing/lexer.ml4
AgeCommit message (Collapse)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Fixing previous commit (something strange happened...)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15423 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Replacing some str with strbrkppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Partial revert of r15148 in order to compile with Camlp4pboutill
+ comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12Remove print call that do not use the pp mechanismpboutill
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
2011-08-13New fix for is_ident_not_keyword.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14410 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09In coqtop, a terminating "." must now be followed by a blank or eof.letouzey
This way, we forbid contiguous sentences like "tac.{tac.}", which should now be written with at least 2 spaces: "tac. {tac. }" This should avoid confusion if a user declare a notation involving ".{" or ".}" as tokens. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14393 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
(an articulating ident needs to be a keyword if the constr entry that preceeds it is higher than the level of applications). Also fixed is_ident_not_keyword which only looked at the first letter and at the keyword status to decide if a token is an ident. This allowed to simplified define_keywords in Metasyntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14389 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Made warning about ending comments in string less intrusive so as to supportherbelin
things like (* "forall X : (* Type *), X" *) without warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13971 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-17About "unsupported" unicode characters in notations.herbelin
- 8.2 (bug-fix): reverted check for unicode early at notation definition time (an unsupported "cadratin" space, 0x2003, was used in CoRN!) [by the way, what to do with unicode spacing characters in general?] - trunk: improved error message, removed redundant code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13561 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
on unsupported unicode character) + forbidding unsupported unicode in Notation declarations too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13526 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
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
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-12Missing warning flush in a lexer message + update of CHANGESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13010 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
2010-03-30Improving error messages in the presence of utf-8 charactersherbelin
- A more clever strategy than the use of null spaces (in revision 12058) for collapsing multi-byte utf-8 characters into one character (toplevel.ml, 8.3 and trunk only) - Fixing discard_to_dot in the presence of iterated lexing failures - Made the lexer state aligned with the start of utf-8 chars instead of staying in the middle of multi-byte chars when a token is not recognized (lexer.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12891 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-04Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)letouzey
- This way, the Makefile.build gets shorter and simplier, with a few nasty hacks removed. - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep". Instead, we now use ocamldep -modules, and process its output via coqdep_boot. This ways, *.cm* of .ml4 are correctly located, even when some .ml files aren't generated yet. - There is no risk of editing the .ml of a .ml4 by mistake, since it is by default in a binary format (cf pr_o.cmo and variable READABLE_ML4). M-x next-error still open the right .ml4 at the right location. - mltop.byteml is now mltop.ml, while mltop.optml keeps its name - .ml of .ml4 are added to .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14- Addition of "Reserved Infix" continued.herbelin
- Tried an extension of the lexer that supports keywords starting with a letter w/o being an ident (e.g. 'U+'). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12326 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-29Miscellaneous practical commits: herbelin
- theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansaspiwack
un plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12147 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-14Fixing #1960 (xml bug with external on goal variable) and #1961herbelin
(anomaly while parsing $ not followed by an ident). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-31allowed patternidents starting with an '_'amahboub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11526 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-30The lexer is changer to break former PATTERNIDENT into two tokens.amahboub
This allows more flexibility in the other uses of the question mark and in particular suppresses the hack for rewriter in g_tactic.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11524 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Autour du parsing:herbelin
- Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalherbelin
alphanumerical symbols) suite à remarques de Arnaud. Correction bugs d'affichage de l'option -translate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11059 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Diverses corrections herbelin
- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev] - suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des quotations de tactiques pour simuler les métas des constr - quitte à devoir utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics] - utilisation de error en place d'un "print_string" d'échec dans fourier - améliorations espérées vis à vis de quelques "bizarreries" dans la gestion des Meta [pretyping] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05Minor fixes: msozeau
- Allow unicode superscripts characters. - Put Program notations in scopes. - Correct priority semantics in typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-18Ajout de caractères unicode reconnus apr le lexernotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10574 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Creation of a new token PATTERNIDENT (?ident) for intro patterns, soglondu
that "intros ? a ? b" behaves as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10155 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Correction boucle du parseur en cas de caractÃère non unicodeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9394 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Correction typo + ajout Arabic Supplementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9015 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10Bug is_numberherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8947 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵notin
(fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-11Oubli des symboles du Latin-1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8805 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-10Centralisation de la détection lettre/symbole par le lexeur dans les plages ↵herbelin
unicode; ajout de nouvelles plages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8800 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Diverses corrections de l'afficheur et du traducteur pour s'assurer deherbelin
la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Ajout de nouvelles plages de symboles unicode; prise en compte des indices ↵herbelin
unicode et letter-like dans les identificateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7870 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Bug (code prévu pour iso-latin et non utf-8)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7869 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-14Code mort du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7865 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Commentaire mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7752 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 10:44:47 +0000