Merge branch 'master' of github.com:ProofGeneral/PG into master_origin

6 files changed, 40 insertions, 12 deletions

diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index bb765c2c..4958b360 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -228,7 +228,9 @@ which can be changed by sending commands.
 In this case, NAME stands for the internal setting, flag, etc,
 for the proof assistant, and a :setting and :type value should be
 provided.  The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string.
+'boolean, 'string. Other types are not supported (see
+`proof-menu-entry-for-setting'). They will yield an error when
+constructing the proof assistant menu.
 
 The function `proof-assistant-format' is used to format VAL.
 
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 3aafa97d..8d93a60b 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -209,7 +209,25 @@ and the function `proof-assistant-format'.  The TYPE item determines
 the form of the menu entry for the setting (this is an Emacs widget type)
 and the DESCR description string is used as a help tooltip in the settings menu.
 
-This list is extended by the `defpacustom' macro.")
+As TYPE's only the simple types boolean, integer, number and
+string are supported (see `proof-menu-entry-for-setting'). Other
+types will yield an error when constructing the proof assistant
+menu from this list.
+
+Customizations defined with `defpacustom' are automatically added
+to this list.")
+
+(defvar proof-assistant-additional-settings nil
+  "Additional proof assistant specific customizations (as list of symbols).
+This variable should hold those proof assistant specific
+customizations that are not included in
+`proof-assistant-settings' but which should be saved/restored
+with the save and reset settings menu entry in the proof
+assistant menu.
+
+Customization variables are missing in `proof-assistant-settings'
+when they have a type not supported by `defpacusom'.")
+
 
 (defvar pg-tracing-slow-mode nil
   "Non-nil for slow refresh mode for tracing output.")
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index d4e0f803..df617347 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -921,8 +921,10 @@ KEY is the optional key binding."
 
 (defun proof-settings-vars ()
   "Return a list of proof assistant setting variables."
-  (mapcar (lambda (setting) (proof-ass-symv (car setting)))
-	  proof-assistant-settings))
+  (append
+   (mapcar (lambda (setting) (proof-ass-symv (car setting)))
+	   proof-assistant-settings)
+   proof-assistant-additional-settings))
 
 (defun proof-settings-changed-from-defaults-p ()
   ;; FIXME: would be nice to add.  Custom support?
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 51038fa6..13da8d98 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -831,7 +831,11 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
   (let ((prover-was-busy nil))
     (unless (proof-shell-live-buffer)
       (error "Proof process not started!"))
-    ;; hook functions might set prover-was-busy
+    ;; Hook functions might set prover-was-busy.
+    ;; In case `proof-action-list' is empty and only
+    ;; `proof-second-action-list-active' is t, the hook functions
+    ;; should clear the queue region and release the proof shell lock.
+    ;; `coq-par-user-interrupt' actually does this.
     (run-hooks 'proof-shell-signal-interrupt-hook)
     (if proof-shell-busy
 	(progn
diff --git a/generic/proof-site.el b/generic/proof-site.el
index c2f9f480..671c3c82 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -39,10 +39,11 @@
 
       (isar "Isabelle" "thy")
       (coq "Coq" "v" nil (".vo" ".glob"))
-      (phox "PhoX" "phx")
+      (easycrypt "EasyCrypt" "ec" ".*\\.eca?")
 
       ;; Obscure instances or conflict with other Emacs modes.
 
+      ;; (phox "PhoX" "phx")
       ;; (lego "LEGO" "l")
       ;; (ccc    "CASL Consistency Checker" "ccc")
 
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 77d3cc33..f0894656 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -842,13 +842,14 @@ The not yet delayed output is in the region
 	 (start proof-shell-delayed-output-start)
 	 (end proof-shell-delayed-output-end)
 	 inst-ex-vars)
-    (when (and (not (memq 'proof-tree-show-subgoal flags))
-	       (> state proof-tree-last-state))
-      ;; Only deal with existentials if the proof assistant has them
-      ;; (i.e., proof-tree-existential-regexp is set) and if there are some
-      ;; goals with existentials.
-      (when (and proof-tree-existential-regexp
+    (unless (memq 'proof-tree-show-subgoal flags)
+      (when (and (> state proof-tree-last-state)
+		 proof-tree-existential-regexp
 		 proof-tree-existentials-alist)
+	;; Only deal with existentials if this is not and undo
+	;; command, if the proof assistant actually has existentials
+	;; (i.e., proof-tree-existential-regexp is set) and if there
+	;; are some goals with existentials.
 	(setq inst-ex-vars
 	      (with-current-buffer proof-shell-buffer
 		(funcall proof-tree-extract-instantiated-existentials