From ecb47478c9f9959ea25ce509076f6e3959d2c620 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Thu, 14 May 2020 15:29:58 +0200 Subject: All case for Show and regex variable --- generic/proof-config.el | 5 +++++ generic/proof-shell.el | 7 +++++-- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'generic') diff --git a/generic/proof-config.el b/generic/proof-config.el index 8d539191..16cdae93 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,6 +399,11 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) +(defcustom proof-show-diffs-regexp nil + "Matches all Show Proof form" + :type 'regexp + :group 'proof-script) + (defcustom proof-save-with-hole-regexp nil "Regexp which matches a command to save a named theorem. The name of the theorem is built from the variable diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a0e80fa7..b6bf9225 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1615,9 +1615,12 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - (setq proof-shell-last-output-kind + ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) + ;; (memq 'empty-action-list flags)) + ;; (setq proof-shell-last-output-kind 'response) ;; only display result for last output - (proof-shell-handle-delayed-output))) + (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) + ;; ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) -- cgit v1.2.3 From aba3f2bfe2bffde6d2df21b098740100459a84be Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 15 May 2020 15:50:48 +0200 Subject: Fix name clash & rephrase some strings --- generic/proof-config.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'generic') diff --git a/generic/proof-config.el b/generic/proof-config.el index 16cdae93..ce72c76c 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,7 +399,7 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) -(defcustom proof-show-diffs-regexp nil +(defcustom proof-show-proof-diffs-regexp nil "Matches all Show Proof form" :type 'regexp :group 'proof-script) -- cgit v1.2.3 From 04aff704f3d13452bc5c52ff860c5ab564539632 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Mon, 18 May 2020 13:33:57 +0200 Subject: WIP for #487 --- generic/proof-shell.el | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b6bf9225..8f23608a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1193,7 +1193,8 @@ contains only invisible elements for Prooftree synchronization." (or (null proof-action-list) (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list))))))) + proof-action-list) + (string= (car (nth 1 item)) "Show."))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1715,7 +1716,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output both)) + (pg-goals-display proof-shell-last-goals-output t)) ;; indicate a goals output has been given 'goals)) -- cgit v1.2.3 From 22681a3caf2c8f45700585ea74dffbf48bb2ac19 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Wed, 20 May 2020 14:19:14 +0200 Subject: Apply reviews of @erikmd --- generic/proof-config.el | 2 +- generic/proof-shell.el | 14 ++++++-------- 2 files changed, 7 insertions(+), 9 deletions(-) (limited to 'generic') diff --git a/generic/proof-config.el b/generic/proof-config.el index ce72c76c..9d352548 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -400,7 +400,7 @@ NB: This setting is not used for matching output from the prover." :group 'proof-script) (defcustom proof-show-proof-diffs-regexp nil - "Matches all Show Proof form" + "Matches all \"Show Proof\" forms (specific to the Coq prover)." :type 'regexp :group 'proof-script) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8f23608a..1258c7f6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1194,7 +1194,8 @@ contains only invisible elements for Prooftree synchronization." (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list) - (string= (car (nth 1 item)) "Show."))))))) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1616,12 +1617,9 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) - ;; (memq 'empty-action-list flags)) - ;; (setq proof-shell-last-output-kind 'response) + (setq proof-shell-last-output-kind ;; only display result for last output - (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) - ;; + (proof-shell-handle-delayed-output))) ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) @@ -1716,7 +1714,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output t)) + (pg-goals-display proof-shell-last-goals-output both)) ;; indicate a goals output has been given 'goals)) -- cgit v1.2.3 From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Mon, 25 May 2020 10:55:03 +0200 Subject: fix: backtrack wrong type argument --- generic/proof-shell.el | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1258c7f6..9e51d4fb 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1181,21 +1181,23 @@ contains only invisible elements for Prooftree synchronization." ;; process the delayed callbacks now (mapc 'proof-shell-invoke-callback cbitems) - (unless (or proof-action-list proof-second-action-list-active) + (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup - (proof-release-lock) - (proof-detach-queue) - (unless flags ; hint after a batch of scripting - (pg-processing-complete-hint)) - (pg-finish-tracing-display)) - - (and (not proof-second-action-list-active) - (or (null proof-action-list) - (cl-every - (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list) - ;; If the last command in proof-action-list is a "Show Proof" form then return t - (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) + (proof-release-lock) + (proof-detach-queue) + (unless flags ; hint after a batch of scripting + (pg-processing-complete-hint)) + (pg-finish-tracing-display)) + + + (and (not proof-second-action-list-active) + (let ((last-command (car (nth 1 (car (last proof-action-list)))))) + (or (null proof-action-list) + (cl-every + (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) + proof-action-list) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd) -- cgit v1.2.3 From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Thu, 28 May 2020 09:21:53 +0200 Subject: fix: backtrack for "Show Proof" disabled --- generic/proof-shell.el | 43 +++++++++++++++++++++---------------------- 1 file changed, 21 insertions(+), 22 deletions(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9e51d4fb..b9ac2b3c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization." (not (memq 'empty-action-list flags)) proof-shell-empty-action-list-command) (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) - (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) - ;; tag all new items with 'empty-action-list - (extra-items (mapcar (lambda (s) (proof-shell-action-list-item - s 'proof-done-invisible - (list 'invisible 'empty-action-list))) - extra-cmds))) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) ;; action-list should be empty at this point (setq proof-action-list (append extra-items proof-action-list)))) @@ -1181,23 +1181,22 @@ contains only invisible elements for Prooftree synchronization." ;; process the delayed callbacks now (mapc 'proof-shell-invoke-callback cbitems) - (unless (or proof-action-list proof-second-action-list-active) + (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup - (proof-release-lock) - (proof-detach-queue) - (unless flags ; hint after a batch of scripting - (pg-processing-complete-hint)) - (pg-finish-tracing-display)) - - - (and (not proof-second-action-list-active) - (let ((last-command (car (nth 1 (car (last proof-action-list)))))) - (or (null proof-action-list) - (cl-every - (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list) - ;; If the last command in proof-action-list is a "Show Proof" form then return t - (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) + (proof-release-lock) + (proof-detach-queue) + (unless flags ; hint after a batch of scripting + (pg-processing-complete-hint)) + (pg-finish-tracing-display)) + + (and (not proof-second-action-list-active) + (let ((last-command (car (nth 1 (car (last proof-action-list)))))) + (or (null proof-action-list) + (cl-every + (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) + proof-action-list) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd) -- cgit v1.2.3