From 325784e32122802b42aff7254423db0ca9509fb4 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 26 Jul 2002 19:42:18 +0000 Subject: Changed a bit more the doc and the CHANGES file, to be consitent. Concerns the coq-user... variables. --- CHANGES | 45 ++++++++++++++++++++++++++++++++------------- 1 file changed, 32 insertions(+), 13 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 06a66c79..960aae1b 100644 --- a/CHANGES +++ b/CHANGES @@ -73,24 +73,43 @@ Commands like Hint, Require, etc, were not backtracked correctly, but are now. Nested proofs and commands nested in proofs are now also well backtracked. -User defined keywords are not completely well backtracked. To solve -this we provide customization, using four configurable variables for -registering personal tactics and commands. Commands and tactics are -split into backable (resp. undoable), i.e. which need "Back" -(resp. "Undo") to be backtracked and not backable (resp. not -undoable). This allows PG to 1) colorize correctly 2) (more important) -to correctly backtrack user-defined commands and tactics. - -See `coq-user-non-backable-commands', `coq-user-backable-commands', -`coq-user-undoable-tactics', `coq-user-non-undoable-tactics' +User defined keywords could not completely well backtracked. The +fall-back mechanism is better now, but to solve this completely we +provide four configurable variables for registering personal tactics +and commands. Commands and tactics are split into state-preserving or +state-changing commands and tactics, i.e. which need or not Back/Undo +to be backtracked. This allows PG to +1) (more important) to correctly backtrack user-defined commands and + tactics. +2) colorize correctly + +See `coq-user-state-preserving-commands, `coq-user-state-changing-commands, +`coq-user-state-preserving-tactics, `coq-user-state-changing-tactics' These variables are regexp lists. See their documentations in emacs of -this variable (C-h v coq-user...) for details on how to set them in -your .emacs file. Example: +this variable (C-h v coq-user...) and in the doc, for details on how +to set them in your .emacs file. Example: + + An example of existing commands that fit each category: + + coq-user-state-preserving-commands: example: "Print" + + coq-user-state-changing-commands: example: "Require" + + coq-user-state-changing-tactics: example: "Intro" + + coq-user-state-preserving-tactics: example: "Proof" + + This variables are string lists. See the documentations in emacs of + this variable (C-h v coq-user...) for details on how to set them + in your .emacs file. - (setq coq-user-backable-commands + Example: + (setq coq-user-state-changing-commands '("MyHint" "MyRequire" "Show\\-+Mydata")) + Last thing: you must restart emacs to allow emacs take these + variable into account. ** Changes for other provers -- cgit v1.2.3