From b72c81f8090c1326fe819ea4c0a2714c0944b8e8 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 29 Jan 2016 14:59:42 +0100
Subject: Import EasyCrypt PG mode

---
 generic/proof-site.el | 1 +
 1 file changed, 1 insertion(+)

(limited to 'generic')

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 521a8d8c..e4fe9096 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -40,6 +40,7 @@
       (isar "Isabelle" "thy")
       (coq "Coq" "v" nil (".vo" ".glob"))
       (phox "PhoX" "phx")
+      (easycrypt "EasyCrypt" "ec" ".*\\.eca?")
 
       ;; Obscure instances or conflict with other Emacs modes.
 
-- 
cgit v1.2.3


From 6d1f608c6e7c39eff89b9461a2f4ea7ff1b19899 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sat, 14 Jan 2017 23:27:24 +0100
Subject: Fix prooftree for Coq 8.6

In Coq 8.6 evar status printing is off by default, causing
prooftree to crash. This patch inserts invisible commands to
switch evar status printing on and off. This is done via the
urgent-action-hook.
---
 coq/coq-system.el     |  12 ++++++
 coq/coq.el            | 112 ++++++++++++++++++++++++++++++++++++++++++++++++--
 generic/proof-tree.el |  13 +++---
 3 files changed, 127 insertions(+), 10 deletions(-)

(limited to 'generic')

diff --git a/coq/coq-system.el b/coq/coq-system.el
index 88ce06be..0b9b6c58 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -170,6 +170,18 @@ Returns nil if the version can't be detected."
 	 (signal 'coq-unclassifiable-version  coq-version-to-use))
 	(t (signal (car err) (cdr err))))))))
 
+(defun coq--post-v86 ()
+  "Return t if the auto-detected version of Coq is >= 8.6.
+Return nil if the version cannot be detected."
+  (let ((coq-version-to-use (or (coq-version t) "8.5")))
+    (condition-case err
+	(not (coq--version< coq-version-to-use "8.6"))
+      (error
+       (cond
+	((equal (substring (cadr err) 0 15) "Invalid version")
+	 (signal 'coq-unclassifiable-version  coq-version-to-use))
+	(t (signal (car err) (cdr err))))))))
+
 (defcustom coq-use-makefile nil
   "Whether to look for a Makefile to attempt to guess the command line.
 Set to t if you want this feature, but note that it is deprecated."
diff --git a/coq/coq.el b/coq/coq.el
index e3541b48..edf905ae 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -24,6 +24,8 @@
   (defvar proof-info nil)       ; dynamic scope in proof-tree-urgent-action
   (defvar action nil)       ; dynamic scope in coq-insert-as stuff
   (defvar string nil)       ; dynamic scope in coq-insert-as stuff
+  (defvar old-proof-marker nil)
+                         ; dynamic scoq in coq-proof-tree-enable-evar-callback
   (defvar coq-auto-insert-as nil)    ; defpacustom
   (defvar coq-time-commands nil)        ; defpacustom
   (defvar coq-use-project-file t)        ; defpacustom
@@ -1851,14 +1853,19 @@ not finished, because Coq 8.5 lists open existential variables
 as (new) open subgoals. For this test we assume that
 `proof-marker' has not yet been moved.
 
+The `proof-tree-urgent-action-hook' is also called for undo
+commands. For those, nothing is done.
+
 The not yet delayed output is in the region
 \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
   ;; (message "CPTGNS start %s end %s"
   ;;          proof-shell-delayed-output-start
   ;;          proof-shell-delayed-output-end)
-  (with-current-buffer proof-shell-buffer
-    (let ((start proof-shell-delayed-output-start)
-          (end proof-shell-delayed-output-end))
+  (let ((start proof-shell-delayed-output-start)
+        (end proof-shell-delayed-output-end)
+        (state  (car proof-info)))
+  (when (> state proof-tree-last-state)
+    (with-current-buffer proof-shell-buffer
       ;; The message "All the remaining goals are on the shelf" is processed as
       ;; urgent message and is therefore before
       ;; proof-shell-delayed-output-start. We therefore need to go back to
@@ -1879,7 +1886,7 @@ The not yet delayed output is in the region
                            '(no-goals-display
                              no-response-display
                              proof-tree-show-subgoal))
-                          proof-action-list)))))))))
+                          proof-action-list))))))))))
   
 (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals)
 
@@ -1916,6 +1923,103 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
     (span-start span-res)))
 
 
+;; In Coq 8.6 the evar line is disabled by default because on some proofs it
+;; causes a severe performance hit. The disabled evar line causes prooftree to
+;; crash with a parsing error. Proof General must therefore turn on the evar
+;; output with the command "Set Printing Dependent Evars Line". Of course,
+;; after the proof, the evar line must be set back to what it was before the
+;; proof. I therefore look in the urgent action hook if proof display is
+;; switched on or off. When switched on, I test the current evar printing
+;; status with the undodumented command "Test Printing Dependent Evars Line" to
+;; remember if I have to switch evar printing off eventually.
+
+(defvar coq--proof-tree-must-disable-evars nil
+  "Remember if evar printing must be disabled when leaving the current proof.")
+
+(defun coq-proof-tree-enable-evar-callback (span)
+  "Callback for the evar printing status test.
+This is the callback for the command ``Test Printing Dependent
+Evars Line''. It checks whether evar printing was off and
+remembers that fact in `coq--proof-tree-must-disable-evars'."
+  (with-current-buffer proof-shell-buffer
+    (save-excursion
+      ;; When the callback runs, the next item is sent to Coq already and
+      ;; therefore proof-marker points to the end of the next command
+      ;; already. proof-shell-filter-manage-output sets old-proof-marker
+      ;; before calling proof-shell-exec-loop, this therefore points to the
+      ;; end of the command of this callback.
+      (goto-char old-proof-marker)
+      (when (re-search-forward "The Printing Dependent Evars Line mode is "
+                               nil t)
+        (if (looking-at "off")
+            (progn
+              ;; (message "CPTEEC evar line mode was off")
+              (setq coq--proof-tree-must-disable-evars t))
+          ;; (message "CPTEEC evar line mode was on")
+          (setq coq--proof-tree-must-disable-evars nil))))))
+
+(defun coq-proof-tree-insert-evar-command (cmd &optional callback)
+  "Insert an evar printing command at the head of `proof-action-list'."
+  (push (proof-shell-action-list-item
+         (concat cmd " Printing Dependent Evars Line.")
+         (if callback callback 'proof-done-invisible)
+         (list 'invisible))
+        proof-action-list))
+
+(defun coq-proof-tree-enable-evars ()
+  "Enable the evar status line for Coq >= 8.6.
+Test the status of evar printing to be able to set it back
+properly after the proof and enable the evar printing."
+  (when (coq--post-v86)
+    ;; We push to proof-action-list --- therefore we need to push in reverse
+    ;; order!
+    (coq-proof-tree-insert-evar-command "Set")
+    (coq-proof-tree-insert-evar-command
+     "Test"
+     'coq-proof-tree-enable-evar-callback)))
+
+(defun coq-proof-tree-disable-evars ()
+  "Disable evar printing if necessary.
+This function switches off evar printing after the proof, if it
+was off before the proof. For undo commands, we rely on the fact
+that Coq itself undos the effect of the evar printing change that
+we inserted after the goal statement. We also rely on the fact
+that Proof General never backtracks into the middle of a
+proof. (If this would happen, Coq would switch evar printing on
+and the code here would not switch it off after the proof.)
+
+Being called from `proof-tree-urgent-action-hook', this function
+can rely on `proof-info' being dynamically bound to the last
+result of `coq-proof-tree-get-proof-info'."
+  (when coq--proof-tree-must-disable-evars
+    (when (> (car proof-info) proof-tree-last-state)
+      (coq-proof-tree-insert-evar-command "Unset"))
+    (setq coq--proof-tree-must-disable-evars nil)))
+
+(defun coq-proof-tree-evar-display-toggle ()
+  "Urgent action hook function for changing the evar printing status in Coq.
+This function is for `proof-tree-urgent-action-hook' (which is
+called only if external proof disaply is switched on). It checks
+whether a proof was started or stopped and inserts commands for
+enableing and disabling the evar status line for Coq 8.6 or
+later. Without the evar status line being enabled, prooftree
+crashes.
+
+Must only be called via `proof-tree-urgent-action-hook' to ensure
+that the dynamic variable `proof-info' is bound to the current
+result of `coq-proof-tree-get-proof-info'."
+  (let ((current-proof-name (cadr proof-info)))
+    (cond
+     ((and (null proof-tree-current-proof) current-proof-name)
+      ;; started a new proof
+      (coq-proof-tree-enable-evars))
+     ((and proof-tree-current-proof (null current-proof-name))
+      ;; finished the current proof
+      (coq-proof-tree-disable-evars)))))
+
+(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle)
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Pre-processing of input string
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
-- 
cgit v1.2.3


From 31a5f3f036d5c15931d7901368b49c60988e9c4e Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Tue, 17 Jan 2017 16:52:10 +0100
Subject: move phox from main to obscure instances

see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I
tried to download phox now, no link was working...
---
 generic/proof-site.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 48a2bdae..671c3c82 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -39,11 +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")
 
-- 
cgit v1.2.3


From 77c3f2eac868f177b73d2aa59b277e40fc48fd0c Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Wed, 18 Jan 2017 22:05:37 +0100
Subject: split emergency-cleanup to handle interrupts properly (fixes #143)

Split coq-par-emergency-cleanup into two functions, one for
reacting on user interrupts and one for cleaning up after
compilation errors.
---
 coq/coq-compile-common.el |  8 ++---
 coq/coq-par-compile.el    | 79 +++++++++++++++++++++++++++++++++++++----------
 generic/proof-shell.el    |  6 +++-
 3 files changed, 71 insertions(+), 22 deletions(-)

(limited to 'generic')

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index af3e70a4..4b0033d1 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -42,9 +42,9 @@ Must be used together with `coq-seq-disable'."
   (add-hook 'proof-shell-extend-queue-hook
 	    'coq-par-preprocess-require-commands)
   (add-hook 'proof-shell-signal-interrupt-hook
-	    'coq-par-emergency-cleanup)
+	    'coq-par-user-interrupt)
   (add-hook 'proof-shell-handle-error-or-interrupt-hook
-	    'coq-par-emergency-cleanup))
+	    'coq-par-user-interrupt))
 
 (defun coq-par-disable ()
   "Disable parallel compilation.
@@ -52,9 +52,9 @@ Must be used together with `coq-seq-enable'."
   (remove-hook 'proof-shell-extend-queue-hook
 	       'coq-par-preprocess-require-commands)
   (remove-hook 'proof-shell-signal-interrupt-hook
-	       'coq-par-emergency-cleanup)
+	       'coq-par-user-interrupt)
   (remove-hook 'proof-shell-handle-error-or-interrupt-hook
-	       'coq-par-emergency-cleanup))
+	       'coq-par-user-interrupt))
 
 (defun coq-seq-enable ()
   "Enable sequential synchronous compilation.
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 8901a008..f9b317c2 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -756,20 +756,15 @@ Used for unlocking ancestors on compilation errors."
 	 (put job 'lock-state 'unlocked)))
      coq--compilation-object-hash)))
 
-(defun coq-par-emergency-cleanup ()
-  "Emergency cleanup for parallel background compilation.
-Kills all processes, unlocks ancestors, clears the queue region
-and resets the internal state."
-  (interactive)				; needed for menu
-  (let (proc-killed was-busy)
+(defun coq-par-kill-and-cleanup ()
+  "Kill all background compilation, cleanup internal state and unlock ancestors.
+This is the common core of `coq-par-emergency-cleanup' and
+`coq-par-user-interrupt'. Returns t if there actually was a
+background job that was killed."
+  (let (proc-killed)
     (when coq--debug-auto-compilation
-      (message "emergency cleanup"))
+      (message "kill all jobs and cleanup state"))
     (setq proc-killed (coq-par-kill-all-processes))
-    (when (and (boundp 'prover-was-busy)
-	       (or proc-killed coq--last-compilation-job
-		   coq--compile-vio2vo-in-progress
-		   coq--compile-vio2vo-delay-timer))
-      (setq prover-was-busy t))
     (setq coq-par-compilation-queue (coq-par-new-queue))
     (setq coq--last-compilation-job nil)
     (setq coq-par-vio2vo-queue (coq-par-new-queue))
@@ -778,12 +773,62 @@ and resets the internal state."
       (cancel-timer coq--compile-vio2vo-delay-timer)
       (setq coq--compile-vio2vo-delay-timer nil))
     (coq-par-unlock-all-ancestors-on-error)
-    (when proof-action-list
-      (setq proof-shell-interrupt-pending t))
-    (proof-release-lock)
-    (proof-detach-queue)
     (setq proof-second-action-list-active nil)
-    (coq-par-init-compilation-hash)))
+    (coq-par-init-compilation-hash)
+    proc-killed))
+
+(defun coq-par-emergency-cleanup ()
+  "Emergency cleanup for errors in parallel background compilation.
+This is the function that cleans everything up when some
+background compilation process detected a severe error. When
+`coq-compile-keep-going' is nil, all errors are severe. When
+`coq-compile-keep-going' is t, coqc and some coqdep errors are
+not severe. This function is also used for the user action to
+kill all background compilation.
+
+On top of `coq-par-kill-and-cleanup', this function resets the
+queue region (and thus `proof-action-list' and signals an
+interrupt to the proof shell."
+  (interactive)				; needed for menu
+  (when coq--debug-auto-compilation
+    (message "emergency cleanup"))
+  (coq-par-kill-and-cleanup)
+  (when proof-action-list
+    (setq proof-shell-interrupt-pending t))
+  (proof-release-lock)
+  (proof-detach-queue))
+
+(defun coq-par-user-interrupt ()
+  "React to a generic user interrupt with cleaning up everything.
+This function cleans up background compilation when the proof
+assistant died (`proof-shell-handle-error-or-interrupt-hook') or
+when the user interrupted Proof General (with C-c C-c or
+`proof-interrupt-process' leading to
+`proof-shell-signal-interrupt-hook').
+
+On top of `coq-par-kill-and-cleanup', this function only sets the
+dynamic variable `prover-was-busy' to tell the proof shell that
+the user actually had a reason to interrupt. However, in the
+special case where `proof-action-list' is nil and
+`coq--last-compilation-job' not, this function also clears the
+queue region and releases the proof shell lock. This has the nice
+side effect, that `proof-interrupt-process' does not send an
+interrupt signal to the prover."
+  (let (proc-killed
+	(was-busy (or coq--last-compilation-job
+		      coq--compile-vio2vo-in-progress
+		      coq--compile-vio2vo-delay-timer)))
+    (when coq--debug-auto-compilation
+      (message "cleanup on user interrupt"))
+    (setq proc-killed (coq-par-kill-and-cleanup))
+    (unless proof-action-list
+      (when coq--debug-auto-compilation
+	(message "clear queue region and proof shell lock"))
+      (proof-release-lock)
+      (proof-detach-queue))
+    (when (and (boundp 'prover-was-busy)
+	       (or proc-killed was-busy))
+      (setq prover-was-busy t))))
 
 (defun coq-par-process-filter (process output)
   "Store output from coq background compilation."
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
-- 
cgit v1.2.3


From 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Thu, 19 Jan 2017 11:40:28 +0100
Subject: save settings not defined with defpacustom (fixes #142)

- infrastructure for saving/resetting customizations not defined
  with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
---
 coq/coq-abbrev.el         | 90 ++++++++++++++++++++++++++++++++---------------
 coq/coq-compile-common.el | 21 ++++++++---
 coq/coq.el                |  6 ++++
 doc/PG-adapting.texi      |  4 +--
 doc/ProofGeneral.texi     | 14 ++++++--
 generic/pg-pamacs.el      |  4 ++-
 generic/pg-vars.el        | 20 ++++++++++-
 generic/proof-menu.el     |  6 ++--
 8 files changed, 124 insertions(+), 41 deletions(-)

(limited to 'generic')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 534c013d..2b318dea 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -169,34 +169,68 @@ It was constructed with `proof-defstringset-fn'.")
 		   coq-compile-parallel-in-background)
       :help ,(concat "Continue background compilation after "
 		     "the first error as far as possible")]
-    ["no quick"
-      (customize-set-variable 'coq-compile-quick 'no-quick)
-      :style radio
-      :selected (eq coq-compile-quick 'no-quick)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile without -quick but accept existion .vio's"]
-     ["quick no vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-no-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
-     ["quick and vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-and-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
-     ["ensure vo"
-      (customize-set-variable 'coq-compile-quick 'ensure-vo)
-      :style radio
-      :selected (eq coq-compile-quick 'ensure-vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Ensure only vo's are used for consistency"]
+     ("Quick compilation"
+      ["no quick"
+       (customize-set-variable 'coq-compile-quick 'no-quick)
+       :style radio
+       :selected (eq coq-compile-quick 'no-quick)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile without -quick but accept existion .vio's"]
+      ["quick no vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-no-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
+      ["quick and vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-and-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
+      ["ensure vo"
+       (customize-set-variable 'coq-compile-quick 'ensure-vo)
+       :style radio
+       :selected (eq coq-compile-quick 'ensure-vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Ensure only vo's are used for consistency"]
+      )
+     ("Auto Save"
+      ["Query coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-coq)
+       :active coq-compile-before-require
+       :help "Ask for each coq-mode buffer, except the current buffer"]
+      ["Query all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-all)
+       :active coq-compile-before-require
+       :help "Ask for all buffers"]
+      ["Autosave coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-coq)
+       :active coq-compile-before-require
+       :help "Save all Coq buffers without confirmation, except the current one"]
+      ["Autosave all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-all)
+       :active coq-compile-before-require
+       :help "Save all buffers without confirmation"]
+      )
+     ["Lock Ancesotors"
+      coq-lock-ancestors-toggle
+      :style toggle
+      :selected coq-lock-ancestors
+      :active coq-compile-before-require
+      :help "Lock files of imported modules"]
      ["Confirm External Compilation"
       coq-confirm-external-compilation-toggle
       :style toggle
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 4b0033d1..72a16881 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -246,7 +246,10 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes
 ensure-vo        Ensure that all library dependencies are present as .vo
                  files and delete outdated .vio files or .vio files that
                  are more recent than the corresponding .vo file. This
-                 setting is the only one that ensures soundness."
+                 setting is the only one that ensures soundness.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Quick compilation'."
   :type
   '(radio
     (const :tag "don't use -quick but accept existing vio files" no-quick)
@@ -371,7 +374,10 @@ This makes four permitted values: 'ask-coq to confirm saving all
 modified Coq buffers, 'ask-all to confirm saving all modified
 buffers, 'save-coq to save all modified Coq buffers without
 confirmation and 'save-all to save all modified buffers without
-confirmation."
+confirmation.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Auto Save'."
   :type
   '(radio
     (const :tag "ask for each coq-mode buffer, except the current buffer"
@@ -389,17 +395,24 @@ confirmation."
   "If non-nil, lock ancestor module files.
 If external compilation is used (via `coq-compile-command') then
 only the direct ancestors are locked. Otherwise all ancestors are
-locked when the \"Require\" command is processed."
+locked when the \"Require\" command is processed.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Lock Ancestors'."
+
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
 
+;; define coq-lock-ancestors-toggle
+(proof-deftoggle coq-lock-ancestors)
+
 (defpacustom confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-`Coq -> Settings -> Confirm External Compilation'."
+`Coq -> Auto Compilation -> Confirm External Compilation'."
   :type 'boolean
   :group 'coq-auto-compile)
 
diff --git a/coq/coq.el b/coq/coq.el
index edf905ae..f6c67475 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1544,6 +1544,12 @@ Near here means PT is either inside or just aside of a comment."
 ;; FIXME da: Does Coq have a help or about command?
 ;;	proof-info-command "Help"
 
+  ;; Settings not defined with defpacustom because they have an unsupported
+  ;; type.
+  (setq proof-assistant-additional-settings
+        '(coq-compile-quick coq-compile-keep-going
+          coq-compile-auto-save coq-lock-ancestors))
+
   (setq proof-goal-command-p 'coq-goal-command-p
         proof-find-and-forget-fn 'coq-find-and-forget
         pg-topterm-goalhyplit-fn 'coq-goal-hyp
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index cf88d683..44c40549 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -361,7 +361,7 @@ file for the mode, which will be
 where @var{proof-home-directory} is the value of the
 variable @samp{@code{proof-home-directory}}.
 
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
+The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" ".*\\.eca?") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
 @end defopt
 
 
@@ -3258,7 +3258,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
+A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
 If nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 442ce6d5..8dab17f0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4667,8 +4667,9 @@ ancestor.
 You have two choices, if you don't like ancestor locking in its
 default way.
 You can either switch ancestor locking completely off via
+menu @code{Coq -> Auto Compilation -> Lock Ancestors} or
 @code{coq-lock-ancestors} (@ref{Customizing Coq Multiple
-File Support}) or you can generally permit editing in locked
+File Support}). Alternatively, you can generally permit editing in locked
 sections with selecting 
 @code{Proof-General} -> @code{Quick Options} -> @code{Read Only}
 -> @code{Freely Edit} (which will set the option
@@ -4689,7 +4690,8 @@ file.]
 Proof General supports quick compilation only with the parallel
 asynchronous compilation. There are 4 modes that can be
 configured with @code{coq-compile-quick} or by selecting one of
-the radio buttons in the @code{Coq -> Auto Compilation} menu.
+the radio buttons in the @code{Coq -> Auto Compilation -> Quick
+compilation} menu.
 
 Use the default @code{no-quick}, if you have not yet switched to
 @code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
@@ -4824,6 +4826,9 @@ modified Coq buffers, @code{'ask-all} to confirm saving all modified
 buffers, @code{'save-coq} to save all modified Coq buffers without
 confirmation and @code{'save-all} to save all modified buffers without
 confirmation.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Auto Save}.
 @end defvar
 
 
@@ -4899,6 +4904,9 @@ If non-nil, lock ancestor module files.@*
 If external compilation is used (via @samp{@code{coq-compile-command}}) then
 only the direct ancestors are locked. Otherwise all ancestors are
 locked when the "Require" command is processed.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Lock Ancestors}.
 @end defvar
 
 
@@ -4942,7 +4950,7 @@ If set let user change and confirm the compilation command.@*
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-@samp{Coq -> Settings -> Confirm External Compilation}.
+@samp{Coq -> Auto Compilation -> Confirm External Compilation}.
 @end defvar
 
 
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?
-- 
cgit v1.2.3