*** empty log message ***

2 files changed, 75 insertions, 78 deletions

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)))
 )
 
 ;;