From b72c81f8090c1326fe819ea4c0a2714c0944b8e8 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub 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 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. --- generic/proof-tree.el | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'generic') 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 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 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. --- generic/proof-shell.el | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'generic') 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 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 --- generic/pg-pamacs.el | 4 +++- generic/pg-vars.el | 20 +++++++++++++++++++- generic/proof-menu.el | 6 ++++-- 3 files changed, 26 insertions(+), 4 deletions(-) (limited to 'generic') 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