diff options
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-pamacs.el | 4 | ||||
-rw-r--r-- | generic/pg-vars.el | 20 | ||||
-rw-r--r-- | generic/proof-menu.el | 6 | ||||
-rw-r--r-- | generic/proof-shell.el | 6 | ||||
-rw-r--r-- | generic/proof-site.el | 3 | ||||
-rw-r--r-- | generic/proof-tree.el | 13 |
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 |