aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Collapse)AuthorAge
...
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-allow Time Back* (cf discussion on coq-club)Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
| | | | | | Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Supporting optional byte-mark order in utf-8 files (bug #2757).Gravatar herbelin2012-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15219 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Migrate the backtracking code from ide_slave.ml into a new backtrack.ml. In particular the history stack of commands that used to be there is now non-coqide-specific. ** Adapted commands ** - "Show Script": a basic functional version is restored (and the printing of scripts at Qed in coqtop). No indentation, one Coq command per line, based on the vernac_expr asts recorded in the history stack, printed via Ppvernac. - "Back n" : now mimics the backtrack of coqide: it goes n steps back (both commands and proofs), and maybe more if needed to avoid re-entering a proof (it outputs a warning in this case). - "BackTo n" : still try to go back to state n, but it also handles the proof state, and it may end on some state n' <= n if needed to avoid re-entering a proof. Ideally, it could someday be used by ProofGeneral instead of the complex Backtrack command. ** Compatible commands ** - "Backtrack" is left intact from compatibility with current ProofGeneral. We simply re-synchronize the command history stack after each Backtrack. - "Undo" is kept as a standard command, not a backtracking one, a bit like "Focus". Same for "Restart" and "Abort". All of these are now accepted in coqide (Undo simply triggers a warning). - Undocumented command "Undo To n" (counting from start of proof instead of from end) also keep its semantics, it is simply made compatible with the new stack mechanism. ** New restrictions ** We now forbid backtracking commands (Reset* / Back*) inside files when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail. Too much work dealing with these situation that nobody uses. ** Internal details ** Internally, the command stack differs a bit from what was in Ide_slave earlier (which was inspired by lisp code in ProofGeneral). We now tag commands that are unreachable by a backtrack, due to some proof being finished, aborted, restarted, or partly Undo'ed. This induce a bit of bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code is straightforward: we simply search backward the first reachable state starting from the desired place. We don't depend anymore on the proof names (apart in the last proof block), It's more robust this way (think of re-entering a M.foo from an outside proof foo). Many internal clarifications in Lib, Vernac, etc. For instance "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls (Lib.label_before_name "foo"), and performs a BackTo to the corresponding label. Concerning Coqide, we directly suppress the regular printing of goals via a flag in Vernacentries. This avoid relying on a classification of commands in Ide_slave as earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail: discard the effects of a successful command (fix #2682)Gravatar letouzey2012-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added checksums to glob files and warned about possibly missingGravatar herbelin2011-10-29
| | | | | | packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 09:27:28 +0000