aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Collapse)AuthorAge
* More work on error handlingGravatar letouzey2011-05-17
| | | | | | | | | | | | | | Anomalies are now meant to be the exceptions that are *not* catched and handled by the new Errors.handle_stack. Three variants of [Errors.print] allow to customize how anomalies are treated. In particular, [Errors.print_no_anomaly] is used for the Fail command, instead of a classification function Cerrors.is_user_error which wasn't customizable. No more AnomalyOnError, its only occurrence is now a regular anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair the "Fail" command after recent changes in exception handlingGravatar letouzey2011-05-16
| | | | | | | | | | | | For that, I introduce a explicit classification function is_user_error : exn -> bool, instead of the previous hack of explain_exn_default_aux (fun () -> raise e). By the way, clean a bit explain_exn_default_aux : many cases are just printed fine by default's Printexn.to_string (for example Not_found). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14129 85f007b7-540e-0410-9357-904b9bb8a0f7
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
| | | | | | | | | | | Local/Global modifiers in interpretation loop so as to support Local/Global for grammar extension) that made use of DuringSyntaxChecking error wrapper inappropriately nested with the DuringCommandInterp error wrapper, what disturbed the error processors. Good thing, we can now simplify things and completely remove the DuringSyntaxChecking wrapper. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail, when successful, prints something only in verbose modeGravatar glondu2010-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid raising an anomaly when an error encapsulated with a dummyGravatar herbelin2010-10-03
| | | | | | location is raised from a loaded/compiled file! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
| | | | | | | | | | | | | | | | | too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 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
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | 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
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
| | | | | | | | | | | | | | | | | | | | | | | "Fail cmd" is similar to "Time cmd", but instead of printing the execution time, it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with an error. This was, we can demonstrate erroneous commands in a script for pedagogical or testing purpose without having to comment it in order to play the rest of the script in coqide/PG. Coq < Fail Foo. The command has indeed failed with message: => Error: Unknown command of the non proof-editing mode. Coq < Fail Check Prop. Prop : Type Error: The command has not failed ! Two more remarks: - Fail doesn't catch anomalies. - Yes it it possible to write things like Fail Fail ... :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
| | | | | | | | | | | | | Coq use case are mostly thoses : - parsing a char stream to get a vernac expr - evaluating a vernac expr with backtracking - turning a knob with a vernac expr, no backtracking - loading an entire file - compiling an entire file - backtracking (no clean API for this yet) - peeking Coq state info (no clean API for this yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Timeout message was not always displayedGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11960 85f007b7-540e-0410-9357-904b9bb8a0f7
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
| | | | | | | | | | modifiers (added a "Syntax Checking" phase for raising a non interpretation error just after a dot is parsed -- maybe exaggerated complication for what we want to do ?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
| | | | | | | | | | 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
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
| | | | | | | | Jean-Marc, feel free to check I've not broken anything concerning coqdoc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added frozen state after each command.Gravatar courtieu2008-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les warnings (ajout Options.warn déclenchée par ↵Gravatar herbelin2007-02-24
| | | | | | | | | compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
| | | | | | current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
| | | | | | | | chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + svnpropGravatar notin2006-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵Gravatar notin2006-06-08
| | | | | | (fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (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
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 'Time Load foo'Gravatar herbelin2004-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5759 85f007b7-540e-0410-9357-904b9bb8a0f7
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5575 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection table des locations lors de Load (pour coqdoc)Gravatar herbelin2004-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5237 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5149 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug: faut brancher la sortie des tactiques sur stdout pendant traductionGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place traduction des tactiques apres evaluation pour permettre des ↵Gravatar herbelin2003-11-09
| | | | | | changements semantiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4839 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug traduction de auto.(simpl). en auto.simpl.Gravatar barras2003-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4676 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups! ca compile maintenantGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4656 85f007b7-540e-0410-9357-904b9bb8a0f7
* translator avoids printing a . followed by a ( by inserting a spaceGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4655 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 16:07:28 +0000