diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-11-29 17:47:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-11-29 17:47:48 +0000 |
| commit | 323f902f3adc747c2787ebfd5a4f50e90e288406 (patch) | |
| tree | 9327af47523d8bd27337627b292c7ce33e66d6be /generic/pg-pbrpm.el | |
| parent | 024b1b5c5063e70222342617042cb482126dfb08 (diff) | |
pg-pbrpm-run-command: use proof-insert-pbp-command
Diffstat (limited to 'generic/pg-pbrpm.el')
| -rw-r--r-- | generic/pg-pbrpm.el | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index eae6a52e..094b18b6 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -1,6 +1,6 @@ ;; pg-pbrpm.el --- Proof General - Proof By Rules Pop-up Menu - mode. ;; -;; Copyright (C) 2004 - Universite de Savoie, France. +;; Copyright (C) 2004, 2009 - Universite de Savoie, France. ;; Authors: Jean-Roch SOTTY, Christophe Raffalli ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; @@ -335,19 +335,22 @@ The prover command is processed via pg-pbrpm-run-command." (progn (pg-pbrpm-erase-buffer-menu) (delete-frame))) - (let (span) - (pop-to-buffer proof-script-buffer) - (proof-activate-scripting) - (proof-goto-end-of-locked) - (proof-activate-scripting) - (insert (concat "\n" command)) - (setq span (span-make (proof-locked-end) (point))) - ; TODO : define the following properties for PBRPM, I don't understand their use ... - (span-set-property span 'type 'pbp) - (span-set-property span 'cmd command) - (proof-start-queue (proof-unprocessed-begin) (point) - (list (list span (list command) - 'proof-done-advancing)))))) + ;; da: why not just this? + (pop-to-buffer proof-script-buffer) + (let ((proof-one-command-per-line t)) + (proof-insert-pbp-command command)))) + ;; (let (span) + ;; (pop-to-buffer proof-script-buffer) + ;; (proof-goto-end-of-locked) + ;; (proof-activate-scripting nil 'advancing) + ;; (insert (concat "\n" command)) + ;; (setq span (span-make (proof-locked-end) (point))) + ;; ; TODO : define the following properties for PBRPM, I don't understand their use ... + ;; (span-set-property span 'type 'pbp) + ;; (span-set-property span 'cmd command) + ;; (proof-start-queue (proof-unprocessed-begin) (point) + ;; (list (list span (list command) + ;; 'proof-done-advancing)))))) ;;--------------------------------------------------------------------------;; ;; Click Informations extractors |