From df57a722603aa5c28645fa983116a7eb67617b0b Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Wed, 9 Feb 2005 14:18:45 +0000 Subject: *** empty log message *** --- phox/phox-pbrpm.el | 146 +++++++++++++++++++++++++++-------------------------- phox/phox.el | 7 +-- 2 files changed, 75 insertions(+), 78 deletions(-) (limited to 'phox') diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 9a18969b..6a3dbdc7 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -36,19 +36,49 @@ (char-equal char (int-char 187))) ) -;;--------------------------------------------------------------------------;; -;; Testing Menu -;;--------------------------------------------------------------------------;; - (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 (mapcar - (lambda (s) (progn (cons order (split-string s "\\\\-")))) + (lambda (s) (append (list order) (split-string s "\\\\-") + (list 'phox-pbrpm-rename-in-cmd))) (split-string str "\\\\\\\\")))) +(defun phox-pbrpm-rename-in-cmd (cmd spans) + (let ((modified nil) (prev 0)) + (mapc (lambda (span) + (if (not (string= (span-property span 'original-text) + (span-string span))) + (setq modified (cons span modified)))) spans) + (setq modified (reverse modified)) + (if modified + (progn + (if (= 0 (span-property (car modified) 'goalnum)) + (progn + (while (and modified (= 0 (span-property (car modified) 'goalnum))) + (let ((span (pop modified))) + (setq cmd (concat cmd ";; rename " + (span-property span 'original-text) " " + (span-string span))))) + (if modified (setq cmd (concat "(" cmd ")"))))) + (if modified (setq cmd (concat cmd ";; "))) + (while modified + (let* ((span (pop modified)) + (goalnum (span-property span 'goalnum))) + (while (< (+ prev 1) goalnum) + (setq cmd (concat cmd "idt @+@ ")) + (setq prev (+ prev 1))) + (setq cmd (concat cmd "(rename " (span-property span 'original-text) " " + (span-string span))) + (setq prev goalnum) + (if (or (not modified) (< goalnum (span-property (car modified) 'goalnum))) + (setq cmd (concat cmd ") @+@ ")) + (setq cmd (concat cmd ";; "))))) + (if (> prev 0) (setq cmd (concat cmd "idt")))))) + cmd) + (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 @@ -72,16 +102,13 @@ (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."))) + (list 4 (phox-lang-absurd) (concat goal-prefix "by_absurd;; elim False"))) (phox-pbrpm-menu-from-string 0 (concat "menu_intro " - (int-to-string (nth 0 click-infos)) - ".")) + (int-to-string (nth 0 click-infos)))) (phox-pbrpm-menu-from-string 0 (concat "menu_evaluate " - (int-to-string (nth 0 click-infos)) - ".")) + (int-to-string (nth 0 click-infos)))) ); end append );end setq );end if @@ -98,35 +125,39 @@ (setq tmp (concat tmp " " (nth 1 region-info)))) region-infos) - tmp) - "."))))) + 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"))) (not region-infos)) - (progn + (let ((r (proof-shell-invisible-cmd-get-result (concat "is_hypothesis " + (int-to-string (nth 0 click-infos)) + " \"" + (nth 1 click-infos) + "\"")))) (setq pbrpm-rules-list (append pbrpm-rules-list - (list - (list 9 (concat "Supprimer l'hypothèse " (nth 1 click-infos) " devenue inutile.") (concat "rmh " (nth 1 click-infos) "."))) + (if (char= (string-to-char r) ?t) + (list + (list 9 (phox-lang-suppress (nth 1 click-infos)) + (concat "[" (int-to-string (nth 0 click-infos)) "] " + "rmh " (nth 1 click-infos)))) + nil) (phox-pbrpm-menu-from-string 1 (concat "menu_elim " (int-to-string (nth 0 click-infos)) " " - (nth 1 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) - ".")) + (nth 1 click-infos))) (phox-pbrpm-menu-from-string 0 (concat "menu_left " (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos) - ".")))))) + (nth 1 click-infos))))))) ; if clicking on an hypothesis with a selection (if (and @@ -144,8 +175,7 @@ (setq tmp (concat tmp " \"" (nth 2 region-info) "\""))) region-infos) - tmp) - ".")) + tmp))) (phox-pbrpm-menu-from-string 1 (concat "menu_rewrite_hyp " (int-to-string (nth 0 click-infos)) " " @@ -155,8 +185,7 @@ (setq tmp (concat tmp " " (nth 1 region-info)))) region-infos) - tmp) - "."))))) + tmp)))))) ; is clicking on a token (if (not (string= (nth 2 click-infos) "")) @@ -164,12 +193,12 @@ (int-to-string (nth 0 click-infos)) " \"" (nth 2 click-infos) - "\".")))) + "\"")))) (if (char= (string-to-char r) ?t) (setq pbrpm-rules-list (append pbrpm-rules-list (list (list 1 (concat - "Ouvre la définition: " + (phox-lang-opendef) (nth 2 click-infos)) (concat goal-prefix @@ -177,6 +206,7 @@ (string= (nth 1 click-infos) "whole")) "unfold " (concat "unfold_hyp " (nth 1 click-infos) " ")) + "$" (nth 2 click-infos) ". "))))) (message (nth 2 click-infos)) @@ -185,9 +215,7 @@ (setq pbrpm-rules-list (append pbrpm-rules-list (list (list 0 (concat - "Instancie " - (nth 2 click-infos) - " avec " + (phox-lang-instance (nth 2 click-infos)) (nth 2 (car region-infos))) (concat goal-prefix @@ -197,50 +225,23 @@ (nth 2 (car region-infos)) ". "))))))))) + + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list + (list 10 "Trivial ?" (concat goal-prefix "trivial")) + (list 10 (phox-lang-prove) (concat goal-prefix "prove") + (lambda (cmd spans) + (let ((span (pop spans))) + (concat cmd " " (span-string span))))) + (list 10 (phox-lang-let) (concat goal-prefix "local") + (lambda (cmd spans) + (let ((span1 (pop spans)) (span2 (pop spans))) + (concat cmd " " (span-string span1) " = "(span-string span2)))))))) + pbrpm-rules-list )) -;;--------------------------------------------------------------------------;; -;; Selections Buffer management -- unused for now -;;--------------------------------------------------------------------------;; -;initialize the selections buffer for the PBRPM mode -;1 buffer for every selections -;(display-buffer (generate-new-buffer (generate-new-buffer-name "phox-selections"))) - -;copy the current region in the selections buffer -(defun pg-pbrpm-add-selection () -"Append the selection of the current buffer to -the phox-selections buffer used with PBRPM." - (interactive) - ;TODO : check wether the selected region is a well formed expression - ;copy at the end of the selections buffer before switching to it - ; else we'll loose mark & point - (switch-to-buffer (get-buffer "phox-selections")) - (goto-char (point-max)) - (insert-string (get-selection)) - ; if the selected region already ends with a \n, don't insert a second one - (if (not (bolp)) - (insert-string "\n")) - (insert-string "\n") - ;buffer is ready to receive a new selection -) - -;clean the phox-selections buffer -(defun pg-pbrpm-clean-selections-buffer () -"Clean the phox-selections buffer used with PBRPM." - (interactive) - (erase-buffer (get-buffer "phox-selections")) -) - -;selections management menu -(defvar phox-pbrpm-menu -"Phox menu for dealing with Selections." - '("Selections" - ["Add Selection" pg-pbrpm-add-selection ] - ["Clean Selections buffer" pg-pbrpm-clean-selections-buffer ] - ) -) ;see phox.el > menu-entries - ;;--------------------------------------------------------------------------;; ;; phox specific functions @@ -252,5 +253,6 @@ the phox-selections buffer used with PBRPM." ;;--------------------------------------------------------------------------;; (require 'pg-pbrpm) +(require 'phox-lang) (provide 'phox-pbrpm) ;; phox-pbrpm ends here \ No newline at end of file diff --git a/phox/phox.el b/phox/phox.el index 3bdf250d..f9645e0e 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -96,12 +96,7 @@ phox-tags-menu (cons phox-extraction-menu - (cons - phox-pbrpm-menu -;; not useful ? -; '(["Delete symbol around cursor" phox-delete-symbol-around-point t] -; ["Delete symbol" phox-delete-symbol t]) - nil)))) + nil))) ) ;; -- cgit v1.2.3