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

7 files changed, 276 insertions, 59 deletions

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 af3e70a4..72a16881 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.
@@ -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-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/coq/coq-syntax.el b/coq/coq-syntax.el
index 5aa41292..5844be74 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -411,7 +411,9 @@ so for the following reasons:
 (defvar coq-decl-db
   '(
     ("Local Axiom" nil "Local Axiom # : #" t "Local\\s-+Axiom")
+    ("Local Axioms" nil "Local Axioms # , #: #" t "Local\\s-+Axioms")
     ("Axiom" "ax" "Axiom # : #" t "Axiom")
+    ("Axioms" "axs" "Axioms # , #: #" t "Axioms")
     ("Global Variable" "gv" "Global Variable #: #." t "Global\\s-+Variable")
     ("Global Variables" "gvs" "Global Variables # , #: #." t "Global\\s-+Variables")
     ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors")
@@ -427,10 +429,11 @@ so for the following reasons:
     ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis")
     ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses")
     ("Parameter" "par" "Parameter #: #" t "Parameter")
-    ("Parameters" "par" "Parameter #: #" t "Parameters")
+    ("Parameters" "par" "Parameters #: #" t "Parameters")
     ("Conjecture" "conj" "Conjecture #: #." t "Conjecture")
     ("Variable" "v" "Variable #: #." t "Variable")
     ("Variables" "vs" "Variables # , #: #." t "Variables")
+    ("Context" nil "Context #, (# : #)." t "Context")
     ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion")
     ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion")
     )
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..f6c67475 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
@@ -1542,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
@@ -1851,14 +1859,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 +1892,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 +1929,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/coq/coqtags b/coq/coqtags
index 6d874e9d..76b5bcc9 100755
--- a/coq/coqtags
+++ b/coq/coqtags
@@ -52,7 +52,7 @@ while(<>)
        { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; }
 
     elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/)
-      { do adddecs($stmt,$1) }
+      { adddecs($stmt,$1); }
 
     elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/)
        { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }