*** empty log message ***

3 files changed, 213 insertions, 121 deletions

diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index bcdb78a5..a6498cce 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -11,8 +11,34 @@
 (defvar pg-pbrpm-use-buffer-menu t
   "if t, pbrpm will use a menu displayed in a dialog fram instead of a popup menu")
 (defvar pg-pbrpm-buffer-menu nil)
+(defvar pg-pbrpm-spans nil)
 (defvar pg-pbrpm-goal-description nil)
 
+(defun pg-pbrpm-erase-buffer-menu ()
+  (save-excursion
+    (set-buffer pg-pbrpm-buffer-menu)
+    (mapc 'delete-span pg-pbrpm-spans)
+    (setq pg-pbrpm-spans nil)
+    (erase-buffer pg-pbrpm-buffer-menu)))
+
+(defun pg-pbrpm-menu-change-hook (start end len)
+  (save-excursion
+    (let ((span (span-at (- start 1) 'editable)))	
+      (if (not span) (setq span (span-at start 'editable)))
+      (if span
+	  (let ((len (- (span-end span) (span-start span))))
+	    (mapc (lambda (sp)
+		    (let* ((p1 (span-start sp))
+			   (p2 (span-end sp))
+			   (spl (span-at p1 'pglock)))
+		      (span-read-write spl)
+		      (goto-char p1)
+		      (insert (span-string span))
+		      (delete-region (+ p1 len) (+ p2 len))
+		      (span-read-only spl)))
+		  (span-property span 'occurrences)))))))
+
+ 
 (defun pg-pbrpm-create-reset-buffer-menu ()
   "Create if necessary and erase all text in the buffer menu"
   (if (or (not pg-pbrpm-buffer-menu) (not (buffer-live-p pg-pbrpm-buffer-menu)))
@@ -23,8 +49,9 @@
 	(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)
+	(make-local-hook 'after-change-functions)
+	(setq after-change-functions (cons 'pg-pbrpm-menu-change-hook after-change-functions)))
+    (pg-pbrpm-erase-buffer-menu))
   (set-buffer pg-pbrpm-buffer-menu))
 
 (defun pg-pbrpm-analyse-goal-buffer ()
@@ -136,50 +163,116 @@ The prover command is processed via pg-pbrpm-run-command."
 			     (append pbrpm-menu-desc
 				     (list (vector
 					    description
-					    (list 'pg-pbrpm-run-command command)))))))
+					    (list 'pg-pbrpm-run-command (list command nil nil))))))))
 					; finally display the pop-up-menu
 		   (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)))
+		       (command (pop pbrpm-list-car))
+		       (act (pop pbrpm-list-car))
 		       (pos (point)))
+		   (setq count (+ 1 count))
 		   (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-string " ") ; hack for renaming of last name
+		   (let ((spans (pg-pbrpm-setup-span pos (point))))
+		     (insert-gui-button (make-gui-button 
+					 (concat (int-to-string count) ")")
+					 'pg-pbrpm-run-command (list command act spans)) pos))
 		   (insert "\n")))
 		 (insert-gui-button (make-gui-button 
 				   "Cancel" 
-				   (lambda (n) (erase-buffer pg-pbrpm-buffer-menu) (delete-frame)) nil))
+				   (lambda (n) (pg-pbrpm-erase-buffer-menu) (delete-frame)) nil))
 		 (x-symbol-decode)
+		 (mapc 'span-read-only pg-pbrpm-spans)
 		 (make-dialog-frame '(width 80 height 30)))
 	       (beep)))))
 
-(defun pg-pbrpm-run-command (command)
+(defun pg-pbrpm-setup-span (start end)
+  "Set up the span in the menu buffer."
+  (save-excursion 
+    (let ((rank 0) (spans nil) (allspan (make-span start end)))
+      (while (< start end)
+	(goto-char start)		    
+	(let ((pos (search-forward "\\[" end 0)) (goalnum 0))
+	  (if pos (progn 
+		    (delete-backward-char) (delete-backward-char)
+		    (setq end (- end 2))
+		    (setq pos (- pos 2))))
+	  (message "make l span %d %d" start (if pos pos end))
+	  (let ((span (make-span start (if pos pos end))))
+	    (set-span-property span 'pglock t)
+	    (setq pg-pbrpm-spans (cons span pg-pbrpm-spans)))
+	  (if pos 
+	      (progn
+		(search-forward "\\]" end)
+		(delete-backward-char) (delete-backward-char)
+		(setq end (- end 2))
+		(setq start (point))
+		(save-excursion
+		  (goto-char pos)
+		  (if (search-forward-regexp "\\\\|\\([0-9]\\)" start t)
+		      (progn
+			(setq goalnum (string-to-int (match-string 1)))
+			(let ((len (- (match-end 0) (match-beginning 0))))
+			  (setq end (- end len))
+			  (setq start (- start len)))
+			(delete-region (match-beginning 0) (match-end 0)))))
+		(let* ((span (make-span pos start))
+		       (str (concat "\\{" (span-string span) 
+				    (if (= goalnum 0) "" 
+				      (concat "\\|" (int-to-string goalnum)))
+				    "\\}"))
+		       (len (- start pos))
+		       (occurrences nil))
+		(save-excursion
+		  (goto-char pos)
+		  (while (search-forward str end t)
+		    (setq end (+ (- end (- (match-end 0) (match-beginning 0))) len))
+		    (delete-region (match-beginning 0) (match-end 0))
+		    (insert (span-string span))
+		    (message "span o %d %d"  (match-beginning 0) (+ (match-beginning 0) len))
+		    (setq occurrences (cons (make-span (match-beginning 0) (+ (match-beginning 0) len)) 
+					   occurrences))))
+		(message "make w span %d %d %s %d" pos start (span-string span) goalnum)
+		(setq spans (cons span spans))
+		(setq rank (+ rank 1))
+		(set-span-property span 'editable t)
+		(set-span-property span 'rank rank)
+		(set-span-property span 'goalnum goalnum)
+		(set-span-property span 'occurrences occurrences)
+		(set-span-property span 'original-text (span-string span))
+		(set-span-property span 'face 'pg-pbrpm-menu-input-face)))
+	    (setq start (if pos pos end)))))
+      (cons allspan (sort (reverse spans) (lambda (sp1 sp2) 
+				  (< (span-property sp1 'goalnum) 
+				     (span-property sp1 'goalnum))))))))
+  
+(defun pg-pbrpm-run-command (args)
 "Insert COMMAND into the proof queue and then run it.
 -- adapted from proof-insert-pbp-command --"
-   (if pg-pbrpm-use-buffer-menu 
-       (progn
-	 (erase-buffer pg-pbrpm-buffer-menu)
-	 (delete-frame)))
-   (set-buffer proof-script-buffer)
-   (proof-activate-scripting)
-   (let (span)
-      (proof-goto-end-of-locked)
-      (set-buffer proof-script-buffer)
-      (proof-activate-scripting)
-      (insert (concat "\n" command))
-      (setq span (make-span (proof-locked-end) (point)))
+   (let* ((command (pop args)) (act (pop args)) (spans (pop args)) (allspan (pop spans)))
+     (if act (setq command (apply act command spans nil)))
+     (if allspan (setq command (concat "(* " (span-string allspan) " *)\n" command ".")))
+     ; delete buffer (and its span) after applying "act"
+     (if pg-pbrpm-use-buffer-menu 
+	 (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 (make-span (proof-locked-end) (point)))
       ; TODO : define the following properties for PBRPM, I don't understand their use ...
-      (set-span-property span 'type 'pbp)
-      (set-span-property span 'cmd command)
-      (proof-start-queue (proof-unprocessed-begin) (point)
-         (list (list span command 'proof-done-advancing))))
-)
+       (set-span-property span 'type 'pbp)
+       (set-span-property span 'cmd command)
+       (proof-start-queue (proof-unprocessed-begin) (point)
+			  (list (list span command 'proof-done-advancing))))))
 
 ;;--------------------------------------------------------------------------;;
 ;; Click Informations extractors
@@ -191,7 +284,7 @@ The prover command is processed via pg-pbrpm-run-command."
     s if either the hypothesis name, \"none\" (for the conclusion) of \"whole\" in strange cases"
   (let ((l pg-pbrpm-goal-description)
 	(found nil))
-    (while (and l (not found)) 
+    (while (and pos l (not found)) 
       (setq start-goal (car l))
       (setq end-goal (cadr l))
       (setq goal-name (caddr l))
@@ -273,7 +366,6 @@ The prover command is processed via pg-pbrpm-run-command."
 (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)
@@ -297,6 +389,14 @@ The prover command is processed via pg-pbrpm-run-command."
   "*Face for showing (multiple) selection."
   :group 'proof-faces)
 
+(defface pg-pbrpm-menu-input-face
+  (proof-face-specs
+   (:background "Gray80")
+   (:background "Gray65")   
+   (: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
@@ -348,20 +448,15 @@ The prover command is processed via pg-pbrpm-run-command."
 	 (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 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 buffer start end)))
-	      (progn
-		(message "2%s" (pg-pbrpm-region-expression buffer start end))
-		(list 0 "none" (pg-pbrpm-region-expression buffer start end)))))
-	(progn
-	  (message "3%s" (pg-pbrpm-region-expression buffer start end))
-	  (list 0 "none" (pg-pbrpm-region-expression buffer start end)))))))
+	     (progn
+	       (setq r (pg-pbrpm-get-region-info start end))
+	       (if r 
+		   (list
+		    (string-to-int (car r)) ; should not be an int for other prover
+		    (cdr r)
+		    (pg-pbrpm-region-expression buffer start end))
+		 (list 0 "none" (pg-pbrpm-region-expression buffer start end))))
+	   (list 0 "none" (pg-pbrpm-region-expression buffer start end))))))
 
 (defun pg-pbrpm-process-regions-list ()
   (pg-pbrpm-do-remember-region (point-marker) (mark-marker))
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)))
 )
 
 ;;