diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-assoc.el | 4 | ||||
| -rw-r--r-- | generic/pg-goals.el | 59 | ||||
| -rw-r--r-- | generic/pg-response.el | 8 | ||||
| -rw-r--r-- | generic/proof-config.el | 22 | ||||
| -rw-r--r-- | generic/proof-script.el | 1 |
5 files changed, 60 insertions, 34 deletions
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index deb40e56..546aae3b 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -95,8 +95,8 @@ If pg-subterm-first-special-char is unset, return STRING unchanged." (goto-char start) (proof-replace-string (char-to-string pg-subterm-end-char) "") (goto-char start) - (if pg-topterm-char - (proof-replace-string (char-to-string pg-topterm-char) "")))))) + (if pg-topterm-regexp + (proof-replace-regexp pg-topterm-regexp "")))))) (defun pg-assoc-strip-subterm-markup-buf-old (start end) diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 23bf522e..7602df1f 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -176,8 +176,8 @@ optimisation.) For subterm markup without communication back to the prover, the annotation is not needed, but the first character must still be given. -For proof-by-pointing (PBP) oriented markup, `pg-topterm-char' and -`pg-topterm-goalhyp-fn' should be set. Together these allow +For proof-by-pointing (PBP) oriented markup, `pg-topterm-regexp' and +`pg-topterm-goalhyplit-fn' should be set. Together these allow further active regions to be defined, corresponding to \"top elements\" in the proof-state display. A \"top element\" is currently assumed to be either a hypothesis or a subgoal, and is assumed to occupy @@ -186,13 +186,13 @@ a line (or at least a line). The markup is simply & <goal or hypthesis line in proof state> ^ | - pg-topterm-char + pg-topterm-regexp -And the function `pg-topterm-goalhyp-fn' is called to do the +And the function `pg-topterm-goalhyplit-fn' is called to do the further analysis, to return an indication of the goal/hyp and record a name value. These values are used to construct PBP commands which can be sent to the prover." - (if pg-subterm-start-char + (if (or pg-subterm-start-char pg-topterm-regexp) ;; markup for topterm alone (let* ((cur start) (len (- end start)) @@ -203,16 +203,19 @@ commands which can be sent to the prover." (while (< cur end) (setq c (char-after cur)) (cond - ;; Seen goal char: this is the start of a top extent - ;; (assumption or goal) - ((= c pg-topterm-char) + ;; Seen goal regexp: this is the start of a top extent + ;; (assumption, goal, literal command) + ((save-excursion + (goto-char cur) + (looking-at pg-topterm-regexp)) (setq topl (cons cur topl)) (setq ap 0)) ;; Seen subterm start char: it's followed by a char ;; indicating the length of the annotation prefix ;; which can be shared with the previous subterm. - ((= c pg-subterm-start-char) + ((and pg-subterm-start-char ;; ignore if subterm start not set + (= c pg-subterm-start-char)) (incf cur) (if pg-subterm-anns-use-stack (setq ap (- ap (- (char-after cur) 128))) @@ -256,9 +259,9 @@ commands which can be sent to the prover." ;; Proof-by-pointing markup assumes "top" elements which define a ;; context for a marked-up (sub)term: we assume these contexts to ;; be either a subgoal to be solved or a hypothesis. - ;; Top element spans are only made if pg-topterm-goalhyp-fn is set. + ;; Top element spans are only made if pg-topterm-goalhyplit-fn is set. ;; NB: If we want Coq pbp: (setq coq-current-goal 1) - (if pg-topterm-goalhyp-fn + (if pg-topterm-goalhyplit-fn (while (setq ap (car topl) topl (cdr topl)) (pg-goals-make-top-span ap (car topl)))) @@ -272,17 +275,26 @@ commands which can be sent to the prover." "Make a top span (goal/hyp area) for mouse active output." (let (span typname) (goto-char start) - ;; skip the pg-topterm-char itself - (forward-char) + ;; skip the pg-topterm-regexp itself + (if (looking-at pg-topterm-regexp) + (forward-char (- (match-end 0) (match-beginning 0)))) ;; typname is expected to be a cons-cell of a type (goal/hyp) ;; with a name, retrieved from the text immediately following - ;; the topterm-char annotation. - (setq typname (funcall pg-topterm-goalhyp-fn)) - (beginning-of-line) ;; any reason why? + ;; the topterm-regexp annotation. + (let ((topterm (point))) + (setq typname (funcall pg-topterm-goalhyplit-fn)) ;; should be non-nil! + (goto-char topterm)) (setq start (point)) - (goto-char end) - (beginning-of-line) - (backward-char) + (if (eq (car-safe typname) 'lit) + ;; Use length of literal command for end point + (forward-char (length (cdr typname))) + ;; Otherwise, use start/end of line before next annotation/buffer end + (goto-char start) + (beginning-of-line) + (setq start (point)) + (goto-char end) ;; next annotation/end of buffer + (beginning-of-line) + (backward-char)) (setq span (make-span start (point))) (set-span-property span 'mouse-face 'highlight) (set-span-property span 'proof-top-element typname))) @@ -374,9 +386,14 @@ user types by hand." ;; Switch focus to another subgoal; a non-scripting command (proof-shell-invisible-command (format pbp-hyp-command (cdr top-info)))) - (t + ((eq (car top-info) 'goal) + ;; A scripting command to change goal (proof-insert-pbp-command - (format pg-goals-change-goal (cdr top-info)))))))) + (format pg-goals-change-goal (cdr top-info)))) + ((eq (car top-info) 'lit) + ;; A literal command to insert + (proof-insert-pbp-command (cdr top-info))))))) + (defun pg-goals-get-subterm-help (spanorwin &optional obj pos) diff --git a/generic/pg-response.el b/generic/pg-response.el index 66c7869a..f6511c6e 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -27,6 +27,7 @@ (setq proof-buffer-type 'response) ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2 (make-local-variable 'font-lock-keywords) + (define-key proof-response-mode-map [(button1)] 'pg-goals-button-action) (define-key proof-response-mode-map [q] 'bury-buffer) (define-key proof-response-mode-map [c] 'pg-response-clear-displays) (make-local-hook 'kill-buffer-hook) @@ -309,6 +310,13 @@ Returns non-nil if response buffer was cleared." (setq start (point)) (insert str) (unless (bolp) (newline)) + + ;; Do pbp markup here + ;; This is added for recommender/sledgehammer like features + ;; NB: bad (slow) behaviour in case user has response buffer + ;; accumulating output and not cleared automatically + (pg-goals-analyse-structure (point-min) (point-max)) + (proof-fontify-region start (point)) ;; This is one reason why we don't keep the buffer in font-lock ;; minor mode: it destroys this hacky property as soon as it's diff --git a/generic/proof-config.el b/generic/proof-config.el index ddcc8cf2..1db9569f 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1308,12 +1308,12 @@ you only need to set if you use that function (by not customizing :type 'string :group 'proof-script) -(defcustom pg-topterm-goalhyp-fn nil - "Function which returns cons cell if point is at a goal/hypothesis. +(defcustom pg-topterm-goalhyplit-fn nil + "Function which returns cons cell if point is at a goal/hypothesis/literal command. This is used to parse the proofstate output to mark it up for -proof-by-pointing. It should return a cons or nil. First element of -the cons is a symbol, 'goal' or 'hyp'. The second element is a -string: the goal or hypothesis itself. +proof-by-pointing or literal command insertion. It should return a cons or nil. +First element of the cons is a symbol, 'goal', 'hyp' or 'lit'. +The second element is a string: the goal, hypothesis, or literal command itself. If you leave this variable unset, no proof-by-pointing markup will be attempted." @@ -1974,7 +1974,7 @@ The default value is \"\\n\" to match up to the end of the line." At the moment, this setting is not used in the generic Proof General. -In the future it will be used for a generic implementation for `pg-topterm-goalhyp-fn', +In the future it will be used for a generic implementation for `pg-topterm-goalhyplit-fn', used to help parse the goals buffer to annotate it for proof by pointing." :type '(choice regexp (const :tag "Unset" nil)) :group 'proof-shell) @@ -2476,13 +2476,13 @@ See `pg-subterm-start-char'." :type 'character :group 'proof-goals) -(defcustom pg-topterm-char nil - "Annotation character that indicates the beginning of a \"top\" element. +(defcustom pg-topterm-regexp nil + "Annotation regexp that indicates the beginning of a \"top\" element. A \"top\" element may be a sub-goal to be proved or a named hypothesis, -for example. It is currently assumed (following LEGO/Coq conventions) -to span a whole line. +for example. It could also be a literal command to insert and +send back to the prover. -The function `pg-topterm-goalhyp-fn' examines text following this +The function `pg-topterm-goalhyplit-fn' examines text following this special character, to determine what kind of top element it is. This setting is also used to see if proof-by-pointing features diff --git a/generic/proof-script.el b/generic/proof-script.el index 893a9f6a..aaa1b98e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2209,6 +2209,7 @@ appropriate." (proof-activate-scripting) (let (span) (proof-goto-end-of-locked) + (insert "\n") ;; could be user opt (insert cmd) (setq span (make-span (proof-locked-end) (point))) (set-span-property span 'type 'pbp) |