work on proof by contextual menu for phox

4 files changed, 435 insertions, 367 deletions

diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index a0da139d..5b609d1d 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -5,6 +5,82 @@
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 
+;; analysis of the goal buffer
+
+
+(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-goal-description nil)
+
+(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)))
+      (progn
+	(setq pg-pbrpm-buffer-menu
+	      (generate-new-buffer (generate-new-buffer-name "*proof-menu*")))
+	(set-buffer pg-pbrpm-buffer-menu)
+	(phox-mode)))
+  (erase-buffer pg-pbrpm-buffer-menu)
+  (set-buffer pg-pbrpm-buffer-menu))
+
+(defun pg-pbrpm-analyse-goal-buffer ()
+  "This function analyses the goal buffer and produces a table to find goals and hypothesis.
+   If stores, in the variable pg-pbrpm-goal-description, a list with shape
+
+   (start-goal end-goal goal-name start-concl hyps ...) with 5 elements for each goal:
+
+     start-goal: the position of the first char of the goal
+     end-goal: the position of the last char of the goal
+     goal-name: the goal name (or number)
+     start-concl: the position of first char of the conclusion of the goal
+     hyps: the list of hypothesis with the shape:
+       
+  (start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elemets per hypothesis:
+     start-hyp: the position of the first char of the hypothesis (including its name)
+     start-hyp-text: the position of the first char of the hypothesis formula (no name)
+     end-hyp: the position of the last char of the hypothesis
+     hyp-name: then name of the hypothesis.
+"
+  (save-excursion
+    (set-buffer proof-goals-buffer)
+    (goto-char 0)
+    (let 
+	((goals nil))
+      (progn 
+	(while (search-forward-regexp pg-pbrpm-start-goal-regexp nil t)
+	  (let
+	      ((hyps nil)
+	       (start-goal (match-end 0))
+	       (goal-num (match-string pg-pbrpm-start-goal-regexp-par-num))
+	       (end-goal (search-forward-regexp pg-pbrpm-end-goal-regexp nil t)))
+	    (goto-char start-goal)
+	    (while (search-forward-regexp pg-pbrpm-start-hyp-regexp end-goal t)
+	      (let
+		  ((start-hyp (match-beginning 0))
+		   (start-hyp-text (match-end 0))
+		   (hyp-name (match-string pg-pbrpm-start-hyp-regexp-par-num))
+		   (end-hyp (- (if
+				(search-forward-regexp pg-pbrpm-start-hyp-regexp end-goal t)
+				(match-beginning 0)
+			      (search-forward-regexp pg-pbrpm-start-concl-regexp end-goal t)
+			      (match-beginning 0)) 1)))
+		(goto-char start-hyp-text)
+		(setq hyps 
+		      (append
+		       (list start-hyp start-hyp-text end-hyp hyp-name) 
+		       hyps))))
+	    
+	    (setq goals 
+		  (append
+		   (list start-goal end-goal goal-num 
+			 (search-forward-regexp pg-pbrpm-start-concl-regexp nil t) hyps)
+		   goals))))
+	  (setq pg-pbrpm-goal-description goals)))))
+
+(add-hook 'proof-shell-handle-delayed-output-hook 'pg-pbrpm-analyse-goal-buffer)
+
+
 ;;--------------------------------------------------------------------------;;
 ;; the Rules Popup Menu functions
 ;;--------------------------------------------------------------------------;;
@@ -13,7 +89,6 @@
 "This function is bound to a CTRL-RightClick in the Proof General goals buffer."
    (interactive "e")
    (save-excursion
-   (proof-pbrpm-regexps)
    (pg-pbrpm-build-menu event (point-marker) (mark-marker))
    )
 )
@@ -22,32 +97,54 @@
 "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).
 The prover command is processed via pg-pbrpm-run-command."
    ;first, run the prover specific (name, rule)'s list generator
-   (setq pbrpm-list 
-      (proof-pbrpm-generate-menu
-         (pg-pbrpm-process-click event) ; retrieve click informations
-         (pg-pbrpm-process-region start end) ; retrieve selected region informations
-      )
-   )
-   ; then make that list a menu description
-   (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))
-            ))
-         )
-      )
-   )
-   ; finally display the pop-up-menu
-   (popup-menu pbrpm-menu-desc)
-)
+   (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))))))
+					; 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)))))))
+					; 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))))))
 
 (defun pg-pbrpm-run-command (command)
 "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)
@@ -67,61 +164,76 @@ The prover command is processed via pg-pbrpm-run-command."
 ;; Click Informations extractors
 ;;--------------------------------------------------------------------------;;
 
-(defun pg-pbrpm-process-click (event)
-"Returns the list of informations about the click needed to call generate-menu. EVENT is an event."
-   (list
-      (pg-pbrpm-click-goal-number event)
-      (pg-pbrpm-click-hyp-or-ccl event)
-      (pg-pbrpm-click-expression event)
-      (pg-pbrpm-click-tree-depth event)
-   )
-)
-
-(defun pg-pbrpm-click-goal-number (event)
-"Number of the goal where the cliked happened"
-   (mouse-set-point event)
-   (search-backward-regexp goal-backward-regexp)
-   (setq str (match-string 0))
-   (string-match goal-number-regexp str)
-   (string-to-int (match-string 0 str))
-)
-
-(defun pg-pbrpm-click-hyp-or-ccl (event)
-"none -> a conclusion, Hyp-name -> an hypothesis, whole -> the whole goal"
-   (mouse-set-point event)
-   (let
-       ((save-point (point))
-	(gl-point (search-backward-regexp goal-backward-regexp 0 t 1)))
-     (goto-char save-point)
-     (if (search-backward-regexp ccl-backward-regexp gl-point t 1)
-	    (identity "none")
-	    (if (search-backward-regexp hyp-backward-regexp 0 t)
-		(match-string 1)
-	      (identity "whole")
-	     )
-      )
-   )
-)
-
-(defun pg-pbrpm-click-expression (event)
-"Valid parenthesis'd expression."
-   (mouse-set-point event)
-   (setq pbrpm-exp-start (event-point event))
-   (setq pbrpm-exp-end (event-point event))
-   ; TODO : add invisible parenthesis management and limits' conditions (regexps)
-;   (while (not (proof-pbrpm-left-paren-p (char-after pbrpm-exp-start)))
-;      (setq pbrpm-exp-start (- pbrpm-exp-start 1)))
-;   (while (not (proof-pbrpm-right-paren-p (char-after pbrpm-exp-end)))
-;      (setq pbrpm-exp-end (+ pbrpm-exp-end 1)))
-   (buffer-substring-no-properties pbrpm-exp-start (+ pbrpm-exp-end 1))
-   ; buffer-substring or buffer-substring-no-properties ?
-)
-
-(defun pg-pbrpm-click-tree-depth (event)
-"Click depth in the tree. If clicking on a parenthesis, the whole expression is considered."
-   (pg-pbrpm-click-or-region-tree-depth (event-point event))
-)
+(defun pg-pbrpm-get-pos-info (pos)
+  "return (n . s) where
+    n is the goal name
+    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)) 
+      (setq start-goal (car l))
+      (setq end-goal (cadr l))
+      (setq goal-name (caddr l))
+      (setq start-concl (cadddr l))
+      (setq hyps (car (cddddr l)))
+      (setq l (cdr (cddddr l)))
+      (if (and (<= start-goal pos) (<= pos end-goal))
+	  (progn
+	    (setq found t)
+	    (setq the-goal-name goal-name))))
+    (if found 
+	(progn  
+	  (if (<= start-concl pos)
+	      (setq the-click-info "none")
+	    (setq found nil)
+	    (while (and hyps (not found))
+	      (setq start-hyp (car hyps))
+	      (setq start-hyp-text (cadr hyps))
+	      (setq end-hyp (caddr hyps))
+	      (setq hyp-name (cadddr hyps))
+	      (setq hyps (cddddr hyps))
+	      (if (and (<= start-hyp pos) (<= pos end-hyp))
+		  (progn 
+		    (setq found t)
+		    (setq the-click-info hyp-name))))
+	    (if (not found)
+		(setq the-click-info "whole")))
+	  (cons the-goal-name the-click-info)))))
 
+(defun pg-pbrpm-get-region-info (start end)
+   "see pg-pbrpm-get-pos-info and source code :-)"
+   (setq r1 (pg-pbrpm-get-pos-info start))
+   (setq r2 (pg-pbrpm-get-pos-info start))
+   (if (and r1 r2 (string-equal (car r1) (car r2)))
+       (if (string-equal (cdr r1) (cdr r2))
+	   r1
+	 (cons (car r1) "whole"))
+     nil))
+	 
+(defun auto-select-arround-pos ()
+  "extract some text arround the current  cursor position"
+  (save-excursion
+    (let ((pos (point)))
+      (beginning-of-line)
+      (block 'loop
+	(while (< (point) pos)
+	  (if (not (search-forward-regexp pg-pbrpm-auto-select-regexp nil t)) (return-from 'loop ""))
+	  (if (and (<= (match-beginning 0) pos) (<= pos (match-end 0)))
+	      (return-from 'loop (match-string 0))))
+	(return-from 'loop "")))))
+    
+(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)))))))
 
 ;;--------------------------------------------------------------------------;;
 ;; Selected Region informations extractors
@@ -131,138 +243,41 @@ The prover command is processed via pg-pbrpm-run-command."
 "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)))
-         (list
-            (pg-pbrpm-region-goal-number start end)
-            (pg-pbrpm-region-hyp-or-ccl start end)
-            (pg-pbrpm-region-expression start end)
-            (pg-pbrpm-region-tree-depth start end)
-         )
-         (progn
-            (set-buffer (marker-buffer start))
-            (list 0 "none" (buffer-substring (marker-position start) (marker-position end)) nil)
-         )
-      )
-      nil ; TODO : define how to manage this error case
-   )
-)
-
-(defun pg-pbrpm-region-goal-number (start end)
-"Goal number of the region"
-   (goto-char (min (marker-position start) (marker-position end)))
-   (search-backward-regexp goal-backward-regexp)
-   (setq str (match-string 0))
-   (string-match goal-number-regexp str)
-   (string-to-int (match-string 0 str))
-)
-
-(defun pg-pbrpm-region-hyp-or-ccl (start end)
-"none -> a conclusion, Hyp-name -> an hypothesis, whole -> the whole goal"
-   (goto-char (min (marker-position start) (marker-position end)))
-   (let
-       ((save-point (point))
-	(gl-point (search-backward-regexp goal-backward-regexp 0 t 1)))
-     (goto-char save-point)
-     (if (search-backward-regexp ccl-backward-regexp gl-point t 1)
-	 (identity "none")
-       (if (search-backward-regexp hyp-backward-regexp 0 t)
-	   (match-string 1)
-         (identity "whole")
-      )
-   )
-))
+	  (progn
+	    (setq r (pg-pbrpm-get-region-info (marker-position start) (marker-position end)))
+	    (if r 
+		(list
+		 (string-to-int (car r)) ; should not be an int for other prover
+		 (cdr r)
+		 (pg-pbrpm-region-expression start end))
+	      (progn
+		(set-buffer (marker-buffer start))
+		(list 0 "none" (pg-pbrpm-region-expression 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
+     ))
 
 (defun pg-pbrpm-region-expression (start end)
 "Valid parenthesis'd expression."
    ; an expression is valid if it has as many left paren' as right paren'
-   (setq
-      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))
-      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 ?
-   )
-)
-
-(defun pg-pbrpm-region-tree-depth (start end)
-"Region depth in the tree. If beginning the region on a parenthesis, the whole expression is considered."
-   (pg-pbrpm-click-or-region-tree-depth (marker-position start))
-)
-
-
-;;--------------------------------------------------------------------------;;
-;; Generic informations extractors
-;;--------------------------------------------------------------------------;;
-
-(defun pg-pbrpm-click-or-region-tree-depth (position)
-"Click or Region depth in the tree. If the (char-after position) is a parenthesis, the whole expression is considered."
-   ; TODO : check again this algorithm ...
-   (goto-char position)
-   ;first, wether a ccl, hyp or goal, find the forward seeking start point
-   (if (search-backward-regexp ccl-backward-regexp 1 t 1)
-      (setq pbrpm-ccl (match-end 0))
-      (setq pbrpm-ccl 1))
-   (if (search-backward-regexp hyp-backward-regexp 1 t 1)
-      (setq pbrpm-hyp (match-end 0))
-      (setq pbrpm-hyp 1))
-   (if (search-backward-regexp goal-backward-regexp 1 t 1)
-      (setq pbrpm-goal (match-end 0))
-      (setq pbrpm-goal 1))
-   (setq pbrpm-exp-char (max pbrpm-ccl pbrpm-hyp pbrpm-goal))
-
-   ;work the tree depth list out
-   (setq
-      pbrpm-exp-end position
-      pbrpm-depth 0
-      pbrpm-tree-list '())
-   (while (<= pbrpm-exp-char pbrpm-exp-end) ; TODO : check this test ...
-      ; openning parenthesis case
-      (if (proof-pbrpm-left-paren-p (char-after pbrpm-exp-char))
-         (progn
-            (if (= pbrpm-depth (length pbrpm-tree-list))
-               (push 1 pbrpm-tree-list)
-            (setq pbrpm-tree-list (list (+ (car pbrpm-tree-list) 1) (cdr pbrpm-tree-list)))
-            )
-         (setq pbrpm-depth (+ pbrpm-depth 1))
-         )
-      )
-      ; closing parenthesis case
-      (if (proof-pbrpm-right-paren-p (char-after pbrpm-exp-char))
-         (progn
-            (if (< (length pbrpm-tree-list) pbrpm-depth)
-               (setq pbrpm-tree-list (cdr pbrpm-tree-list))
-            )
-            (setq pbrpm-depth (- pbrpm-depth 1))
-         )
-      )
-      (setq pbrpm-exp-char (+ pbrpm-exp-char 1))
-   )
-   (reverse pbrpm-tree-list)
-)
-
-;;--------------------------------------------------------------------------;;
-;; Error messages management
-;;--------------------------------------------------------------------------;;
-
-; unused for now ...
-(defun pg-pbrpm-dialog (message)
-   (make-dialog-box 'question
-   :title "PBRPM-ERROR"
-   :modal t
-   :question message
-   :buttons (list (vector " OK " '(identity nil) t)))
-)
-
-; TODO : use also log messages in the minibuffer ...
-
+   (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 ?
+	 ))))
 
 ;;--------------------------------------------------------------------------;;
 
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el
index de9ee603..5878c937 100644
--- a/phox/phox-pbrpm.el
+++ b/phox/phox-pbrpm.el
@@ -10,14 +10,17 @@
 ;;--------------------------------------------------------------------------;;
 ;; Syntactic functions
 ;;--------------------------------------------------------------------------;;
-(defun phox-pbrpm-regexps ()
-  (setq
-    goal-backward-regexp "^goal [0-9]+/[0-9]+$"
-    goal-number-regexp "[0-9]+"
-    hyp-backward-regexp "[^A-Za-z0-9_.']\\([A-Za-z0-9_.']+\\) :="
-    ccl-backward-regexp "|-")
+(setq
+ pg-pbrpm-start-goal-regexp "^goal \\([0-9]+\\)/[0-9]+\\( (new)\\)?$"
+ pg-pbrpm-start-goal-regexp-par-num 1
+ pg-pbrpm-end-goal-regexp "^$"
+ 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]+\\)"
 )
 
+
 ; TODO : deal with future invisible parentheses (french guillemots)
 (defun phox-pbrpm-left-paren-p (char)
 "Retrun t if the character is a left parenthesis : '(' or a french guillemot '<<'"
@@ -37,6 +40,32 @@
 ;; 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)
+  "build a menu from a string send by phox"
+  (if (string= str "") nil
+    (phox-pbrpm-eliminate-id nil (mapcar 
+				  (lambda (s) (progn (message s) (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
 
@@ -44,136 +73,167 @@
    ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list)
    ;region-infos = idem if in the goal buffer, (0, "none", expression, nil ) if in another buffer, do not display if no region available.
 
-   (setq pbrpm-rules-list (list))
+   (let
+     ((pbrpm-rules-list nil)
+      (goal-prefix
+       (if (= (nth 0 click-infos) 1) "" 
+	 (concat "["
+		 (int-to-string (nth 0 click-infos))
+		 "] "))))
+ 
 
    ; the first goal is the selected one by default, so we prefer not to display it.
 
    ; if clicking in a conclusion => select.intro
-   (if (and (string= (nth 1 click-infos) "none") (not region-infos))
-      (setq pbrpm-rules-list
-         (append pbrpm-rules-list
-            (list
-	     (list "Décompose"
-               (if (= (nth 0 click-infos) 1)
-                  (identity "intro. ")
-                  (concat "select " (int-to-string (nth 0 click-infos)) ". intro. ")))
-	     (list "Décompose plusieurs"
-               (if (= (nth 0 click-infos) 1)
-                  (identity "intros. ")
-                  (concat "select " (int-to-string (nth 0 click-infos)) ". intros. ")))
-		  );end list's
-            ); end append
-      );end setq
-   );end if
-
-   ; if clicking in an hypothesis => select.elim
-   (if (and
-         (not (or (string= (nth 1 click-infos) "none")
-            (string= (nth 1 click-infos) "whole")))
-         (not region-infos))
-      (progn 
-       (setq pbrpm-rules-list
-	     (append pbrpm-rules-list
-		     (list (list "Produit la conclusion"
-               (if (= (nth 0 click-infos) 1)
-                  (concat "elim "
-                     (nth 1 click-infos)
-                     ". ")
-                  (concat "select "
-                     (int-to-string (nth 0 click-infos))
-                     ". elim "
-                     (nth 1 click-infos)
-                     ". "))))))
-      (setq pbrpm-rules-list
-         (append pbrpm-rules-list
-            (list (list "QED"
-               (if (= (nth 0 click-infos) 1)
-                  (concat "axiom "
-                     (nth 1 click-infos)
-                     ". ")
-                  (concat "select "
-                     (int-to-string (nth 0 click-infos))
-                     ". axiom "
-                     (nth 1 click-infos)
-                     ". "))))))))
+     (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))
+				  "."))))
+		       ); end append
+	       );end setq
+       );end if
 
-   ; if clicking in an hypothesis => select.left
-   (if (and
-         (not (or (string= (nth 1 click-infos) "none")
+					; if clicking in an hypothesis => select.elim
+     (if (and
+	  (not (or (string= (nth 1 click-infos) "none")
+		   (string= (nth 1 click-infos) "whole")))
+	  (not region-infos))
+	 (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))
-      (setq pbrpm-rules-list
-      (append pbrpm-rules-list
-         (list (list "Décompose"
-            (if (= (nth 0 click-infos) 1)
-		(concat "left "
-			(nth 1 click-infos)
-                     ". ")
-               (concat "select "
-		       (int-to-string (nth 0 click-infos))
-		       ". left"
-		  (nth 1 click-infos)
-                     ". ")
- 		  ))
-	       (list "Décompose plusieurs"
-            (if (= (nth 0 click-infos) 1)
-		(concat "lefts "
-			(nth 1 click-infos)
-                     ". ")
-               (concat "select "
-		       (int-to-string (nth 0 click-infos))
-		       ". lefts"
-		  (nth 1 click-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)
+				  "."))))))))
 
    ; if region is an hypothesis (ie in the goals buffer) and clicking in that hyp's goal =>
-   (if region-infos
-   (if (and
-         (not (or (string= (nth 1 region-infos) "none")
-            (string= (nth 1 region-infos) "whole")))
-         (equal (nth 0 click-infos) (nth 0 region-infos))
-      )
-      (setq pbrpm-rules-list
-         (append pbrpm-rules-list
-            (list (list "Réécrit la conclusion"
-               (if (= (nth 0 click-infos) 1)
-                  (concat "rewrite "
-                     (nth 1 region-infos)
-                     ". ")
-                  (concat "select "
-                     (int-to-string (nth 0 click-infos))
-                     ". rewrite "
-                     (nth 1 region-infos)
-                     ". ")))))))
-   )
+;   (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 (not (string= (nth 2 click-infos) ""))
+       (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition "
+							      (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: "
+					(nth 2 click-infos))
+				       (concat 
+					goal-prefix
+					(if (or (string= (nth 1 click-infos) "none") 
+						(string= (nth 1 click-infos) "whole"))
+					    "unfold " 
+					  (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")))
-	(not (string= (nth 2 region-infos) ""))
-	)
+	(nth 2 region-infos))
        (setq pbrpm-rules-list
          (append pbrpm-rules-list
-            (list (list "Applique l'hypothèse à une expression"
-               (if (= (nth 0 click-infos) 1)
-               (concat "apply "
-                  (nth 1 click-infos)
-                  " with "
-                  (nth 2 region-infos)
-                  ". ")
-               (concat "select "
-                  (int-to-string (nth 0 click-infos))
-                  ". select "
-                  (nth 1 click-infos)
-                  " with "
-                  (nth 2 region-infos)
-                  ". ")))))))
+            (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 region-infos
-   (if (and
+   (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")
@@ -182,51 +242,46 @@
          (not (string= (nth 1 click-infos) (nth 1 region-infos)))
       )
       (progn 
-         (setq pbrpm-rules-list
-         (append pbrpm-rules-list
-            (list (list "Réécrit l'hypothèse"
-               (if (= (nth 0 click-infos) 1)
-               (concat "rewrite_hyp "
-                  (nth 1 click-infos)
-                  " "
-                  (nth 1 region-infos)
-                  ". ")
-               (concat "select "
-                  (int-to-string (nth 0 click-infos))
-                  ". rewrite_hyp "
-                  (nth 1 click-infos)
-                  " "
-                  (nth 1 region-infos)
-                  ". "))))))
-       (setq pbrpm-rules-list
-         (append pbrpm-rules-list
-            (list (list "Applique l'hypothèse à une autre hypothèse"
-               (if (= (nth 0 click-infos) 1)
-               (concat "apply "
-                  (nth 1 click-infos)
-                  " with "
-                  (nth 1 region-infos)
-                  ". ")
-               (concat "select "
-                  (int-to-string (nth 0 click-infos))
-                  ". select "
-                  (nth 1 click-infos)
-                  " with "
-                  (nth 1 region-infos)
-                  ". "))))))))
-
-  )
-
-   (identity pbrpm-rules-list)
-)
+	(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)
+				      ". ")))))))
 
+   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")))
+;(display-buffer (generate-new-buffer (generate-new-buffer-name "phox-selections")))
 
 ;copy the current region in the selections buffer
 (defun pg-pbrpm-add-selection ()
@@ -246,7 +301,6 @@ the phox-selections buffer used with PBRPM."
   ;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."
@@ -271,7 +325,6 @@ the phox-selections buffer used with PBRPM."
 (defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu)
 (defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p)
 (defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p)
-(defalias 'proof-pbrpm-regexps 'phox-pbrpm-regexps)
 
 ;;--------------------------------------------------------------------------;;
 (require 'pg-pbrpm)
diff --git a/phox/phox.el b/phox/phox.el
index d5e726e3..a2945c97 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -157,7 +157,7 @@
    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]* goals? created\\)"
+   proof-shell-start-goals-regexp  "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]* new goals?\\)"
    proof-shell-end-goals-regexp  "^End of goals."
    proof-shell-quit-cmd            "quit."
    proof-shell-restart-cmd         "restart."
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
index 84f7d7d1..038b6112 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -71,10 +71,10 @@ See `x-symbol-header-groups-alist'."
    (lambda (x)
      (cons x 
 	   (cond
-	    ;; CW: where are the shapes `id' and `op' used?
+	    ;; the shapes `id' and `op' are used by x-symbol-phox-token-grammar
 	    ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x)
 	     'id)
-	    ((string-match "\\`[<>!+-*/|&]+\\'" x) 
+	    ((string-match "\\`[]><=\\/~&+-*%!{}:-]+\\'" x) 
 	     'op))))
    tokens))