coqide: fenetre de cmmandes . undo correct

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3747 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 109 insertions, 46 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 773fe54f6..065627d89 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -1,23 +1,23 @@
 let commands = [
-  "Abort";
+  ["Abort";
   "Add Abstract Ring";
   "Add Abstract Semi Ring";
   "Add Field";
   "Add LoadPath";
   "Add ML Path";
   "Add Morphism";
-  "Add Printing If ident";
-  "Add Printing Let ident";
+  "Add Printing If";
+  "Add Printing Let";
   "Add Rec LoadPath";
   "Add Rec ML Path";
   "Add Ring";
   "Add Semi Ring";
   "Add Semi Ring";
   "Add Setoid";
-  "Axiom";
-  "Back";
-  "Begin Silent";
-  "Canonical Structure";
+  "Axiom";];
+  ["Back";
+  "Begin Silent";];
+  ["Canonical Structure";
   "Cd";
   "Chapter";
   "Check";
@@ -25,16 +25,16 @@ let commands = [
   "Coercion Local";
   "CoFixpoint";
   "CoInductive";
-  "Correctness";
-  "Declare ML Module";
+  "Correctness";];
+  ["Declare ML Module";
   "Defined";
   "Definition";
   "Derive Dependent Inversion";
   "Derive Dependent Inversion_clear";
   "Derive Inversion";
   "Derive Inversion_clear";
-  "Drop";
-  "End";
+  "Drop";];
+  ["End";
   "End Silent";
   "Eval";
   "Explicitation of implicit arguments";
@@ -44,15 +44,15 @@ let commands = [
   "Extraction Inline";
   "Extraction Language";
   "Extraction Module";
-  "Extraction NoInline";
-  "Fact";
+  "Extraction NoInline";];
+  ["Fact";
   "Fixpoint";
-  "Focus";
-  "Global Variable";
+  "Focus";];
+  ["Global Variable";
   "Goal";
-  "Grammar";
-  "Hint;
-    * Hint Constructors";
+  "Grammar";];
+  ["Hint";
+   "Hint Constructors";
   "Hint Unfold";
   "Hint";
   "Hint Rewrite";
@@ -62,27 +62,27 @@ let commands = [
   "Hints Immediate";
   "Hints Resolve";
   "Hints Unfold";
-  "Hypothesis";
-  "Identity Coercion";
+  "Hypothesis";];
+  ["Identity Coercion";
   "Implicit Arguments Off";
   "Implicit Arguments On";
   "Implicits";
   "Inductive";
   "Infix";
-  "Inspect";
-  "Lemma";
+  "Inspect";];
+  ["Lemma";
   "Load";
   "Load Verbose";
   "Local";
   "Locate";
   "Locate File";
-  "Locate Library";
-  "Module";
+  "Locate Library";];
+  ["Module";
   "Module Type";
-  "Mutual Inductive";
-  "Notation";
-  "Opaque";
-  "Parameter";
+  "Mutual Inductive";];
+  ["Notation";];
+  ["Opaque";];
+  ["Parameter";
   "Print";
   "Print All";
   "Print Classes";
@@ -103,17 +103,17 @@ let commands = [
   "Print Table Printing If";
   "Print Table Printing Let";
   "Proof";
-  "Pwd";
-  "Qed";
-  "Quit";
-  "Read Module";
+  "Pwd";];
+  ["Qed";
+  "Quit";];
+  ["Read Module";
   "Record";
   "Recursive Extraction";
   "Recursive Extraction Module";
   "Remark";
   "Remove LoadPath";
-  "Remove Printing If ident";
-  "Remove Printing Let ident";
+  "Remove Printing If";
+  "Remove Printing Let";
   "Require";
   "Require Export";
   "Reset";
@@ -121,8 +121,8 @@ let commands = [
   "Reset Initial";
   "Restart";
   "Restore State";
-  "Resume";
-  "Save";
+  "Resume";];
+[  "Save";
   "Scheme";
   "Search";
   "Search ... inside ...";
@@ -156,16 +156,16 @@ let commands = [
   "Structure";
   "Suspend";
   "Syntactic Definition";
-  "Syntax";
-  "Tactic Definition";
-  "Test Printing If ident";
-  "Test Printing Let ident";
+  "Syntax";];
+  ["Tactic Definition";
+  "Test Printing If";
+  "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";
   "Theorem";
   "Time";
-  "Transparent";
-  "Undo";
+  "Transparent";];
+  ["Undo";
   "Unfocus";
   "Unset Extraction AutoInline";
   "Unset Extraction Optimize";
@@ -175,8 +175,71 @@ let commands = [
   "Unset Printing Coercions";
   "Unset Printing Synth";
   "Unset Printing Wildcard";
-  "Unset Undo";
-  "Variable";
-  "Variables";
-  "Write State";
+  "Unset Undo";];
+  ["Variable";
+  "Variables";];
+  ["Write State";];
+]
+
+let state_preserving = [
+  "Check";
+  "Eval";
+  "Extract Constant";
+  "Extract Inductive";
+  "Extraction";
+  "Extraction Inline";
+  "Extraction Language";
+  "Extraction Module";
+  "Extraction NoInline";
+  "Inspect";
+  "Print";
+  "Print All";
+  "Print Classes";
+  "Print Coercion Paths";
+  "Print Coercions";
+  "Print Extraction Inline";
+  "Print Graph";
+  "Print Hint";
+  "Print HintDb";
+  "Print LoadPath";
+  "Print ML Modules";
+  "Print ML Path";
+  "Print Module";
+  "Print Module Type";
+  "Print Modules";
+  "Print Proof";
+  "Print Section";
+  "Print Table Printing If";
+  "Print Table Printing Let";
+
+  "Pwd";
+
+  "Search";
+  "SearchAbout";
+  "SearchPattern";
+  "SearchRewrite";
+
+  "Set Printing Coercion";
+  "Set Printing Coercions";
+  "Set Printing Synth";
+  "Set Printing Wildcard";
+
+  "Show";
+  "Show Conjectures";
+  "Show Implicits";
+  "Show Intro";
+  "Show Intros";
+  "Show Proof";
+  "Show Script";
+  "Show Tree";
+
+  "Test Printing If";
+  "Test Printing Let";
+  "Test Printing Synth";
+  "Test Printing Wildcard";
+
+  "Unset Printing Coercion";
+  "Unset Printing Coercions";
+  "Unset Printing Synth";
+  "Unset Printing Wildcard";
 ]