diff options
| -rw-r--r-- | generic/pg-pbrpm.el | 263 | ||||
| -rw-r--r-- | phox/phox-pbrpm.el | 268 | ||||
| -rw-r--r-- | phox/phox.el | 17 |
3 files changed, 286 insertions, 262 deletions
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 5b609d1d..bcdb78a5 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -20,7 +20,10 @@ (setq pg-pbrpm-buffer-menu (generate-new-buffer (generate-new-buffer-name "*proof-menu*"))) (set-buffer pg-pbrpm-buffer-menu) - (phox-mode))) + (phox-mode) + (x-symbol-mode t) ; just to be sure + (font-lock-mode t) ; just to be sure (not activated on OSX ?? + )) (erase-buffer pg-pbrpm-buffer-menu) (set-buffer pg-pbrpm-buffer-menu)) @@ -92,6 +95,17 @@ (pg-pbrpm-build-menu event (point-marker) (mark-marker)) ) ) +(defun pg-pbrpm-exists (f l0) + (if (null l0) nil + (or (funcall f (car l0)) (pg-pbrpm-exists f (cdr l0))))) + +(defun pg-pbrpm-eliminate-id (acc l) + (if (null l) (reverse acc) + (if + (pg-pbrpm-exists (lambda (x) + (string= (car x) (car (car l)))) acc) + (pg-pbrpm-eliminate-id acc (cdr l)) + (pg-pbrpm-eliminate-id (cons (car l) acc) (cdr l))))) (defun pg-pbrpm-build-menu (event start end) "Build a Proof By Rules pop-up menu according to the state of the proof, the event and a selected region (between the start and end markers). @@ -99,44 +113,51 @@ The prover command is processed via pg-pbrpm-run-command." ;first, run the prover specific (name, rule)'s list generator (setq click-info (pg-pbrpm-process-click event start end)) ; retrieve click informations (if click-info - (progn - (setq pbrpm-list - (mapcar 'cdr - (sort - (proof-pbrpm-generate-menu - click-info - (pg-pbrpm-process-region start end)) - (lambda (l1 l2) (< (car l1) (car l2)))))) + (let + ((pbrpm-list + (pg-pbrpm-eliminate-id nil (mapcar 'cdr + (sort + (proof-pbrpm-generate-menu + click-info + (pg-pbrpm-process-regions-list)) + (lambda (l1 l2) (< (car l1) (car l2))))))) + (count 0)) ; retrieve selected region informations ; then make that list a menu description - - (if (not pg-pbrpm-use-buffer-menu) - (progn - (setq pbrpm-menu-desc '("PBRPM-menu")) - (while pbrpm-list - (setq pbrpm-list-car (pop pbrpm-list)) - (setq pbrpm-menu-desc - (append pbrpm-menu-desc - (list (vector - (pop pbrpm-list-car) - (list 'pg-pbrpm-run-command (pop pbrpm-list-car))))))) + (if pbrpm-list + (if (not pg-pbrpm-use-buffer-menu) + (progn + (setq pbrpm-menu-desc '("PBRPM-menu")) + (while pbrpm-list + (let* ((pbrpm-list-car (pop pbrpm-list)) + (description (pop pbrpm-list-car)) + (command (concat "(*" description "*)\n" (pop pbrpm-list-car)))) + (setq pbrpm-menu-desc + (append pbrpm-menu-desc + (list (vector + description + (list 'pg-pbrpm-run-command command))))))) ; finally display the pop-up-menu - (popup-menu pbrpm-menu-desc)) - (pg-pbrpm-create-reset-buffer-menu) - (while pbrpm-list - (setq pbrpm-list-car (pop pbrpm-list)) - (setq description (pop pbrpm-list-car)) - (setq command (pop pbrpm-list-car)) - (setq pos (point)) - (insert-string " ") - (insert-string description) - (insert-gui-button (make-gui-button "Go" 'pg-pbrpm-run-command command) pos) - (insert "\n")) - (insert-gui-button (make-gui-button - "Cancel" - (lambda (n) (erase-buffer pg-pbrpm-buffer-menu) (delete-frame)) nil)) - (x-symbol-decode) - (make-dialog-frame '(width 80 height 30)))))) + (popup-menu pbrpm-menu-desc)) + (pg-pbrpm-create-reset-buffer-menu) + (while pbrpm-list + (let* ((pbrpm-list-car (pop pbrpm-list)) + (description (pop pbrpm-list-car)) + (command (concat "(*" description "*)\n" (pop pbrpm-list-car))) + (pos (point))) + (insert-string " ") + (insert-string description) + (setq count (+ 1 count)) + (insert-gui-button (make-gui-button + (concat (int-to-string count) ")") + 'pg-pbrpm-run-command command) pos) + (insert "\n"))) + (insert-gui-button (make-gui-button + "Cancel" + (lambda (n) (erase-buffer pg-pbrpm-buffer-menu) (delete-frame)) nil)) + (x-symbol-decode) + (make-dialog-frame '(width 80 height 30))) + (beep))))) (defun pg-pbrpm-run-command (command) "Insert COMMAND into the proof queue and then run it. @@ -222,68 +243,162 @@ The prover command is processed via pg-pbrpm-run-command." (return-from 'loop (match-string 0)))) (return-from 'loop ""))))) +(defun pg-pbrpm-translate-position (buffer pos) + "return pos if buffer is goals-buffer otherwise, return the point position in + the goal buffer" + (if (eq proof-goals-buffer buffer) pos + (point proof-goals-buffer))) + (defun pg-pbrpm-process-click (event start end) "Returns the list of informations about the click needed to call generate-menu. EVENT is an event." (save-excursion - (mouse-set-point event) - (let* ((pos (point)) - (r (pg-pbrpm-get-pos-info pos))) - (if r (list - (string-to-int (car r)) ; should not be an int for other prover - (cdr r) - (if (and start end (string-equal (buffer-name proof-goals-buffer) (buffer-name (marker-buffer end))) (<= (marker-position start) pos) (<= pos (marker-position end))) - (pg-pbrpm-region-expression start end) - (auto-select-arround-pos))))))) + (save-window-excursion + (mouse-set-point event) + (let* ((pos (event-point event)) + (buffer (event-buffer event)) + (r (pg-pbrpm-get-pos-info (pg-pbrpm-translate-position buffer pos)))) + (if r (list + (string-to-int (car r)) ; should not be an int for other prover + (if (eq proof-goals-buffer buffer) (cdr r) (auto-select-arround-pos)) + (if (and start end (eq proof-goals-buffer buffer) + (<= (marker-position start) pos) (<= pos (marker-position end))) + (pg-pbrpm-region-expression buffer (marker-position start) + (marker-position end)) + (auto-select-arround-pos)))))))) ;;--------------------------------------------------------------------------;; ;; Selected Region informations extractors ;;--------------------------------------------------------------------------;; +(defvar pg-pbrpm-remember-region-selected-region nil) +(defvar pg-pbrpm-regions-list nil) + +(defun pg-pbrpm-erase-regions-list () + (message "erase list") + (mapc (lambda (span) (delete-span span)) pg-pbrpm-regions-list) + (setq pg-pbrpm-regions-list nil) + nil) + +(add-hook 'mouse-track-drag-up-hook (lambda (event count) + (if (not (member 'control (event-modifiers event))) + (pg-pbrpm-erase-regions-list)))) + +(defun pg-pbrpm-filter-regions-list () + (let ((l pg-pbrpm-regions-list)) + (setq pg-pbrpm-regions-list nil) + (mapc (lambda (span) (if (span-live-p span) + (setq pg-pbrpm-regions-list (cons span pg-pbrpm-regions-list)) + (delete-span span))) l))) -(defun pg-pbrpm-process-region (start end) -"Returns the list of informations about the the selected region needed to call generate-menu. START and END are markers" - (if (and start end) ; if a region is selected - (if (string-equal (buffer-name proof-goals-buffer) (buffer-name (marker-buffer end))) +(defface pg-pbrpm-multiple-selection-face + (proof-face-specs + (:background "orange") + (:background "darkorange") + (:italic t)) + "*Face for showing (multiple) selection." + :group 'proof-faces) + +(defun pg-pbrpm-do-remember-region (start end) + (pg-pbrpm-filter-regions-list) + (if (and start end (not (eq start end))) ; if a region is selected + (let ((span (make-span start end)) + (found nil)) + (setq pg-pbrpm-regions-list (mapcar (lambda (oldspan) + (let ((oldstart (span-start oldspan)) + (oldend (span-end oldspan))) + (if (and (eq (current-buffer) (span-buffer oldspan)) + (or (and (<= start oldstart) (<= oldstart end)) + (and (<= start oldend) (<= oldend end)))) + (progn + (setq found t) + (delete-span oldspan) + span) + oldspan))) pg-pbrpm-regions-list)) + (if (not found) (setq pg-pbrpm-regions-list (cons span pg-pbrpm-regions-list))) + (set-span-property span 'face 'pg-pbrpm-multiple-selection-face)))) + +; the follwing are adapted from mouse-track-insert from mouse.el + +(defun pg-pbrpm-remember-region-drag-up-hook (event click-count) + (setq pg-pbrpm-remember-region-selected-region + (default-mouse-track-return-dragged-selection event))) + +(defun pg-pbrpm-remember-region-click-hook (event click-count) + (default-mouse-track-drag-hook event click-count nil) + (pg-pbrpm-remember-region-drag-up-hook event click-count) + t) + +(defun pg-pbrpm-remember-region (event &optional delete) + "Allow multiple selection as a list of spam stored in ???. The current (standard) + selection in the same buffer is also stored" + (interactive "*e") + (setq pg-pbrpm-remember-region-selected-region nil) + (let ((mouse-track-drag-up-hook 'pg-pbrpm-remember-region-drag-up-hook) + (mouse-track-click-hook 'pg-pbrpm-remember-region-click-hook) + (start (point)) (end (mark))) + (if (and start end) (pg-pbrpm-do-remember-region start end)) + (mouse-track event) + (if (consp pg-pbrpm-remember-region-selected-region) + (let ((pair pg-pbrpm-remember-region-selected-region)) + (pg-pbrpm-do-remember-region (car pair) (cdr pair)))))) + +(defun pg-pbrpm-process-region (span) +"Returns the list of informations about the the selected region needed to call generate-menu. span is a span covering the selected region" + (let ((start (span-start span)) + (end (span-end span)) + (buffer (span-buffer span))) + (if (and start end) ; if a region is selected + (if (eq proof-goals-buffer buffer) (progn - (setq r (pg-pbrpm-get-region-info (marker-position start) (marker-position end))) + (setq r (pg-pbrpm-get-region-info start end)) (if r + (progn (message "1%s %d %d" (pg-pbrpm-region-expression buffer start end) start end) (list (string-to-int (car r)) ; should not be an int for other prover (cdr r) - (pg-pbrpm-region-expression start end)) + (pg-pbrpm-region-expression buffer start end))) (progn - (set-buffer (marker-buffer start)) - (list 0 "none" (pg-pbrpm-region-expression start end))))) + (message "2%s" (pg-pbrpm-region-expression buffer start end)) + (list 0 "none" (pg-pbrpm-region-expression buffer start end))))) (progn - (set-buffer (marker-buffer start)) - (list 0 "none" (pg-pbrpm-region-expression start end)))) - nil ; TODO : define how to manage this error case - )) + (message "3%s" (pg-pbrpm-region-expression buffer start end)) + (list 0 "none" (pg-pbrpm-region-expression buffer start end))))))) -(defun pg-pbrpm-region-expression (start end) +(defun pg-pbrpm-process-regions-list () + (pg-pbrpm-do-remember-region (point-marker) (mark-marker)) + (mapcar (lambda (span) (pg-pbrpm-process-region span)) pg-pbrpm-regions-list)) + +(defun pg-pbrpm-region-expression (buffer start end) "Valid parenthesis'd expression." ; an expression is valid if it has as many left paren' as right paren' - (let - ((pbrpm-region-char (marker-position start)) - (pbrpm-left-pars 0) - (pbrpm-right-pars 0)) - (while (<= pbrpm-region-char (marker-position end)) - (if (proof-pbrpm-left-paren-p (char-after pbrpm-region-char)) - (setq pbrpm-left-pars (+ pbrpm-left-pars 1))) - (if (proof-pbrpm-right-paren-p (char-after pbrpm-region-char)) - (setq pbrpm-right-pars (+ pbrpm-right-pars 1))) - (setq pbrpm-region-char (+ pbrpm-region-char 1))) - (if (= pbrpm-left-pars pbrpm-right-pars) - (buffer-substring (marker-position start) (marker-position end) (marker-buffer start)) - (progn - nil ; TODO : define how to manage this error case - ;we could call (pg-pbrpm-dialog "Selected region is not valid), then what about the state of the process ? - )))) + (buffer-substring start end buffer)) +; (let +; ((pbrpm-left-pars 0) +; (pbrpm-right-pars 0) +; (pos start)) +; (while (< pos end) +; (if (proof-pbrpm-left-paren-p (char-after pos)) +; (setq pbrpm-left-pars (+ pbrpm-left-pars 1))) +; (if (proof-pbrpm-right-paren-p (char-after pos)) +; (setq pbrpm-right-pars (+ pbrpm-right-pars 1))) +; (setq pos (+ pos 1))) +; (if (= pbrpm-left-pars pbrpm-right-pars) +; (buffer-substring start end buffer) +; (progn +; nil ; TODO : define how to manage this error case +; ;we could call (pg-pbrpm-dialog "Selected region is not valid), then what about the state of the process ? +; )))) ;;--------------------------------------------------------------------------;; (require 'pg-goals) (define-key proof-goals-mode-map [(button3)] 'pg-pbrpm-button-action) (define-key proof-goals-mode-map [(control button3)] 'pg-goals-yank-subterm) +(define-key proof-goals-mode-map [(control button1)] 'pg-pbrpm-remember-region) +(define-key pg-span-context-menu-keymap [(button3)] 'pg-pbrpm-button-action) +(define-key pg-span-context-menu-keymap [(control button3)] 'pg-span-context-menu) +(define-key proof-mode-map [(button3)] 'pg-pbrpm-button-action) +(define-key proof-mode-map [(control button3)] 'pg-goals-yank-subterm) +(define-key proof-mode-map [(control button1)] 'pg-pbrpm-remember-region) (provide 'pg-pbrpm) ;; pg-pbrpm ends here
\ No newline at end of file diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 5878c937..9a18969b 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -17,7 +17,7 @@ pg-pbrpm-start-hyp-regexp "^\\([A-Za-z0-9_.']+\\) := " pg-pbrpm-start-hyp-regexp-par-num 1 pg-pbrpm-start-concl-regexp "^ *|- " - pg-pbrpm-auto-select-regexp "\\(\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\(_+\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\)*\\)\\|\\(\\?[0-9]+\\)" + pg-pbrpm-auto-select-regexp "\\(\\(\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\)\\(_+\\(\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\)\\)*\\)\\|\\(\\?[0-9]+\\)" ) @@ -40,31 +40,14 @@ ;; Testing Menu ;;--------------------------------------------------------------------------;; -(defun phox-pbrpm-exists (f l0) - (if (null l0) nil - (or (funcall f (car l0)) (phox-pbrpm-exists f (cdr l0))))) -(defun phox-pbrpm-eliminate-id (acc l) - (if (null l) (reverse acc) - (message "call") - (message (nth 0 (car l))) - (message (nth 1 (car l))) - (if - (phox-pbrpm-exists (lambda (x) - (progn - (message "=") - (message (nth 0 x)) - (message (nth 0 (car l))) - (string= (nth 0 x) (nth 0 (car l))))) acc) - (phox-pbrpm-eliminate-id acc (cdr l)) - (phox-pbrpm-eliminate-id (cons (car l) acc) (cdr l))))) - -(defun phox-pbrpm-menu-from-string (str) +(defun phox-pbrpm-menu-from-string (order str) "build a menu from a string send by phox" + (setq str (proof-shell-invisible-cmd-get-result str)) (if (string= str "") nil - (phox-pbrpm-eliminate-id nil (mapcar - (lambda (s) (progn (message s) (split-string s "\\\\-"))) - (split-string str "\\\\\\\\"))))) + (mapcar + (lambda (s) (progn (cons order (split-string s "\\\\-")))) + (split-string str "\\\\\\\\")))) (defun phox-pbrpm-generate-menu (click-infos region-infos) ; This FAKE function will be replace by a real 'generate-menu' once the code will be judged stable @@ -84,23 +67,41 @@ ; the first goal is the selected one by default, so we prefer not to display it. - ; if clicking in a conclusion => select.intro + ; if clicking in a conclusion with no selection (if (and (string= (nth 1 click-infos) "none") (not region-infos)) (setq pbrpm-rules-list (append pbrpm-rules-list (list (list 10 "Trivial ?" (concat goal-prefix "trivial.")) (list 4 "Par l'absurde" (concat goal-prefix "by_absurd;; elim False."))) - (mapcar (lambda (l) (cons 0 l)) (phox-pbrpm-menu-from-string - (proof-shell-invisible-cmd-get-result - (concat "menu_intro " - (int-to-string (nth 0 click-infos)) - ".")))) + (phox-pbrpm-menu-from-string 0 + (concat "menu_intro " + (int-to-string (nth 0 click-infos)) + ".")) + (phox-pbrpm-menu-from-string 0 + (concat "menu_evaluate " + (int-to-string (nth 0 click-infos)) + ".")) ); end append );end setq );end if - ; if clicking in an hypothesis => select.elim + ; if clicking a conclusion with a selection + (if (and (string= (nth 1 click-infos) "none") region-infos) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (phox-pbrpm-menu-from-string 1 + (concat "menu_rewrite " + (int-to-string (nth 0 click-infos)) " " + (let ((tmp "")) + (mapc (lambda (region-info) + (setq tmp + (concat tmp " " (nth 1 region-info)))) + region-infos) + tmp) + "."))))) + + ; if clicking in an hypothesis with no selection (if (and (not (or (string= (nth 1 click-infos) "none") (string= (nth 1 click-infos) "whole"))) @@ -108,77 +109,56 @@ (progn (setq pbrpm-rules-list (append pbrpm-rules-list - (list (list 3 (concat - "Déduit la conclusion de " - (nth 1 click-infos) - " (génère éventuellement de nouveaux buts) ?") - (concat goal-prefix - "elim " - (nth 1 click-infos) - ". ")) - (list 3 (concat - "Rentre les négations (loi de De Morgan) de " - (nth 1 click-infos) " ?") - (concat goal-prefix "rewrite_hyp " - (nth 1 click-infos) - " demorganl.")) - (list 4 (concat - "Conclustion égale à " - (nth 1 click-infos) " ?") - (concat goal-prefix - "axiom " - (nth 1 click-infos) - ". "))))))) - - ; if clicking in an hypothesis => select.left - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - (not region-infos)) - (progn - (if (char= ?t (string-to-char (proof-shell-invisible-cmd-get-result - (concat "is_equation " - (int-to-string (nth 0 click-infos)) - " \"" - (nth 1 click-infos) - "\".")))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 2 - (concat "Récrit la conclusion avec " - (nth 1 click-infos) - " ?") - (concat goal-prefix - "rewrite " - (nth 1 click-infos) - ". ")))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (mapcar (lambda (l) (cons 0 l)) (phox-pbrpm-menu-from-string - (proof-shell-invisible-cmd-get-result - (concat "menu_left " - (int-to-string (nth 0 click-infos)) - (nth 1 click-infos) - ".")))))))) + (list + (list 9 (concat "Supprimer l'hypothèse " (nth 1 click-infos) " devenue inutile.") (concat "rmh " (nth 1 click-infos) "."))) + (phox-pbrpm-menu-from-string 1 + (concat "menu_elim " + (int-to-string (nth 0 click-infos)) " " + (nth 1 click-infos) + ".")) + (phox-pbrpm-menu-from-string 1 + (concat "menu_evaluate_hyp " + (int-to-string (nth 0 click-infos)) " " + (nth 1 click-infos) + ".")) + (phox-pbrpm-menu-from-string 0 + (concat "menu_left " + (int-to-string (nth 0 click-infos)) + " " + (nth 1 click-infos) + ".")))))) - ; if region is an hypothesis (ie in the goals buffer) and clicking in that hyp's goal => -; (if (and -; region-infos -; (string= (nth 1 click-infos) "none") -; (not (or (string= (nth 1 region-infos) "none") -; (string= (nth 1 region-infos) "whole"))) -; (equal (nth 0 click-infos) (nth 0 region-infos)) -; (string-to-char (proof-shell-invisible-cmd-get-result -; (concat "is_equation " -; (int-to-string (nth 0 region-infos)) -; " \"" -; (nth 1 region-infos) -; "\".")))) -; (setq pbrpm-rules-list -; (append pbrpm-rules-list -; (list (list (concat "Récrit la conclusion avec " (nth 1 region-infos)) -; (concat goal-prefix "rewrite " (nth 1 region-infos) ". ")))))) + ; if clicking on an hypothesis with a selection + (if (and + (not (or (string= (nth 1 click-infos) "none") + (string= (nth 1 click-infos) "whole"))) + region-infos) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (phox-pbrpm-menu-from-string 1 + (concat "menu_apply " + (int-to-string (nth 0 click-infos)) " " + (nth 1 click-infos) + (let ((tmp "")) + (mapc (lambda (region-info) + (setq tmp + (concat tmp " \"" (nth 2 region-info) "\""))) + region-infos) + tmp) + ".")) + (phox-pbrpm-menu-from-string 1 + (concat "menu_rewrite_hyp " + (int-to-string (nth 0 click-infos)) " " + (nth 1 click-infos) + (let ((tmp "")) + (mapc (lambda (region-info) + (setq tmp + (concat tmp " " (nth 1 region-info)))) + region-infos) + tmp) + "."))))) + ; is clicking on a token (if (not (string= (nth 2 click-infos) "")) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition " (int-to-string (nth 0 click-infos)) @@ -199,79 +179,23 @@ (concat "unfold_hyp " (nth 1 click-infos) " ")) (nth 2 click-infos) ". "))))) - (if (and (char= (string-to-char (nth 2 click-infos)) ??) - region-infos) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - "Instancie " - (nth 2 click-infos) - " avec " - (nth 2 region-infos)) - (concat - goal-prefix - "instance " - (nth 2 click-infos) - " " - (nth 2 region-infos) - ". "))))))))) - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - (nth 2 region-infos)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 4 (concat "Applique " - (nth 1 click-infos) - " à l'expression " - (nth 2 region-infos) " ?") - (concat goal-prefix - "apply " - (nth 1 click-infos) - " with " - (nth 2 region-infos) - ". ")))))) - - ; if region is an hypothesis (ie in the goals buffer) and clicking in an (other) hyp', both in the same goal => - (if (and region-infos - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - (not (or (string= (nth 1 region-infos) "none") - (string= (nth 1 region-infos) "whole"))) - (equal (nth 0 click-infos) (nth 0 region-infos)) - (not (string= (nth 1 click-infos) (nth 1 region-infos))) - ) - (progn - (if (char= ?t (string-to-char (proof-shell-invisible-cmd-get-result - (concat "is_equation " - (int-to-string (nth 0 click-infos)) - " \"" - (nth 1 click-infos) - "\".")))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 4 (concat - "Récrit " (nth 1 region-infos) - " avec l'équation " (nth 1 click-infos) " ?") - (concat goal-prefix - "rewrite_hyp " - (nth 1 region-infos) - " " - (nth 1 click-infos) - ". ")))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 4 (concat - "Applique " (nth 1 click-infos) - " avec l'hypothèse " (nth 1 region-infos) " ?") - (concat goal-prefix - "apply " - (nth 1 click-infos) - " with " - (nth 1 region-infos) - ". "))))))) + (message (nth 2 click-infos)) + (if (and (char= (string-to-char (nth 2 click-infos)) ??) + region-infos (not (cdr region-infos))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list 0 (concat + "Instancie " + (nth 2 click-infos) + " avec " + (nth 2 (car region-infos))) + (concat + goal-prefix + "instance " + (nth 2 click-infos) + " " + (nth 2 (car region-infos)) + ". "))))))))) pbrpm-rules-list )) diff --git a/phox/phox.el b/phox/phox.el index a2945c97..3bdf250d 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -157,26 +157,11 @@ proof-shell-prompt-pattern "\\(>phox> \\)\\|\\(%phox% \\)" proof-shell-annotated-prompt-regexp "\\(>phox> \\)\\|\\(%phox% \\)" proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]* new goals?\\)" + proof-shell-start-goals-regexp "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]+ new goals?\\)\\|\\([0-9]+ goals? possibly instanced\\)" proof-shell-end-goals-regexp "^End of goals." proof-shell-quit-cmd "quit." proof-shell-restart-cmd "restart." proof-shell-proof-completed-regexp "^.*^proved" - ;; pg-subterm-first-special-char ?\371 - ;; proof-shell-wakeup-char ?\371 - ;; pg-subterm-start-char ?\371 - ;; pg-subterm-sep-char ?\372 - ;; pg-topterm-char ?\373 - ;; pg-subterm-end-char ?\374 - ;; proof-shell-eager-annotation-start "\376" - ;; proof-shell-eager-annotation-start-length 1 - ;; proof-shell-eager-annotation-end "\377" -; proof-shell-annotated-prompt-regexp "Lego> \371" -; proof-shell-result-start "\372 Pbp result \373" -; proof-shell-result-end "\372 End Pbp result \373" -; proof-shell-start-goals-regexp "\372 Start of Goals \373" -; proof-shell-end-goals-regexp "\372 End of Goals \373" -; proof-shell-pre-sync-init-cmd "Configure AnnotateOn;" )) |