Removed support for x-symbol (I do not like it because it changes the buffer content !)

sym-lock is still available on xemacs only

various other bug fix.

4 files changed, 60 insertions, 30 deletions

diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 9a264b00..6471f3d4 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -1,3 +1,4 @@
+
 ;; $State$ $Date$ $Revision$ 
 ;; syntax
 
@@ -254,10 +255,9 @@ If inside a comment, just process until the start of the comment."
   (interactive)
 ;  (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
   (proof-with-script-buffer
-   (proof-maybe-save-point
     (goto-char (proof-queue-or-locked-end))
-    (proof-assert-next-command))
-   (proof-maybe-follow-locked-end)))
+    (proof-assert-next-command)
+    (proof-maybe-follow-locked-end)))
 
 ;;--------------------------------------------------------------------------;;
 ;; Obtaining some informations on the system.
diff --git a/phox/phox-lang.el b/phox/phox-lang.el
index 952842e5..a67941e4 100644
--- a/phox/phox-lang.el
+++ b/phox/phox-lang.el
@@ -6,8 +6,7 @@
 (provide 'phox-lang)
 
 (defvar phox-lang
-  (let* ((s1 (getenv "LANG")) (s2 (getenv "LC_LANG")) (s (if s1 s1 s2)))
-    (message s)
+  (let* ((s1 (getenv "LANG")) (s2 (getenv "LC_LANG")) (s (substring (if s1 s1 (if s2 s2 "en")) 0 2)))
     (cond
       ((or (string= s "en") (string= s "us")) 'en)
       ((string= s "fr") 'fr)
@@ -21,8 +20,8 @@
 
 (defun phox-lang-suppress (s)
   (case phox-lang
-    (en (concat "Remove hypothesis " s " (if it became useless)."))
-    (fr (concat  "Supprimer l'hypothèse " s " (si elle est devenue inutile)."))))
+    (en (concat "Remove hypothesis " s " (if it became useless)"))
+    (fr (concat  "Supprimer l'hypothèse " s " (si elle est devenue inutile)"))))
 
 (defun phox-lang-opendef ()
   (case phox-lang 
@@ -34,22 +33,27 @@
     (en (concat "Choose " s " = "))
     (fr (concat  "Choisissons " s " = "))))
 
+(defun phox-lang-open-instance (s)
+  (case phox-lang
+    (en (concat "Choose " s " =  \\[ \\]"))
+    (fr (concat  "Choisissons " s " = \\[ \\]"))))
+
 (defun phox-lang-lock (s)
   (case phox-lang
-    (en (concat "Lock variable" s "."))
-    (fr (concat  "Vérouille la variable " s "."))))
+    (en (concat "Lock variable " s))
+    (fr (concat  "Vérouille la variable " s))))
 
 (defun phox-lang-unlock (s)
   (case phox-lang
-    (en (concat "Unlock variable" s "."))
-    (fr (concat  "Dévérouille la variable " s "."))))
+    (en (concat "Unlock variable " s))
+    (fr (concat  "Dévérouille la variable " s))))
 
 (defun phox-lang-prove (s)
   (case phox-lang 
-    (en (concat "Let us prove \\[" s "\\]."))
-    (fr (concat "Prouvons \\[" s "\\]."))))
+    (en (concat "Let us prove \\[" s "\\]"))
+    (fr (concat "Prouvons \\[" s "\\]"))))
 
 (defun phox-lang-let (s)
   (case phox-lang 
-    (en (concat "Let \\[ \\] = \\[" s "\\]."))
-    (fr (concat "Définissons \\[ \\] = \\[" s "\\]."))))
+    (en (concat "Let \\[ \\] = \\[" s "\\]"))
+    (fr (concat "Définissons \\[ \\] = \\[" s "\\]"))))
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el
index fe202166..9c7411f3 100644
--- a/phox/phox-pbrpm.el
+++ b/phox/phox-pbrpm.el
@@ -211,12 +211,24 @@
 				    (phox-lang-instance (nth 2 click-infos))
 				    (nth 2 (car region-infos)))
 				 (concat 
-				  goal-prefix
 				  "instance "
 				  (nth 2 click-infos) 
 				  " "
-				  (nth 2 (car region-infos))
-				  ". "))))))
+				  (nth 2 (car region-infos))))))))
+
+   (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??)
+	    (not region-infos))
+       (setq pbrpm-rules-list
+	     (append pbrpm-rules-list
+		     (list (list 0 (concat 
+				    (phox-lang-open-instance (nth 2 click-infos)))
+				 (concat 
+				  "instance "
+				  (nth 2 click-infos) 
+				  " ")
+			  (lambda (cmd spans) 
+			    (let ((span (pop spans)))
+			      (concat cmd " " (span-string span)))))))))
 
    ; is clicking on a token with no selection
    (if (and (not region-infos) (not (string= (nth 2 click-infos) "")))
@@ -241,8 +253,7 @@
 					    "unfold -ortho " 
 					  (concat "unfold_hyp " (nth 1 click-infos) " -ortho "))
 					"$"
-					(nth 2 click-infos)
-					". ")))))
+					(nth 2 click-infos))))))
 	   (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??))
 	       (let  ((r (proof-shell-invisible-cmd-get-result (concat "is_locked "
 							      (nth 2 click-infos)))))
@@ -253,16 +264,14 @@
 					 (concat 
 					  goal-prefix
 					  "unlock "
-					  (nth 2 click-infos)
-					  ". ")))))
+					  (nth 2 click-infos))))))
 		     (setq pbrpm-rules-list
 			   (append pbrpm-rules-list
 				   (list (list 0 (phox-lang-lock (nth 2 click-infos))
 					 (concat 
 					  goal-prefix
 					  "lock "
-					  (nth 2 click-infos)
-					  ". ")))))))))))
+					  (nth 2 click-infos))))))))))))
 
    (let ((arg (if (and region-infos (not (cdr region-infos))) (nth 2 (car region-infos)) " ")))
      (setq pbrpm-rules-list
diff --git a/phox/phox.el b/phox/phox.el
index 1f8c2ef1..be6714fa 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -139,7 +139,7 @@
    proof-find-and-forget-fn        'phox-find-and-forget
    proof-find-theorems-command      "search \"%s\"."
    proof-auto-multiple-files       nil
-   font-lock-keywords              (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
+   font-lock-keywords              phox-font-lock-keywords
    )
   (phox-init-syntax-table)
   (setq pbp-goal-command "intro %s;")
@@ -194,8 +194,7 @@
 (define-derived-mode phox-response-mode proof-response-mode
   "PhoX response" nil
   (setq 
-   proof-resp-font-lock-keywords 
-   (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
+   proof-resp-font-lock-keywords phox-font-lock-keywords
    proof-output-fontify-enable     t)
   (phox-sym-lock-start)
   (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
@@ -206,9 +205,8 @@
 
 (define-derived-mode phox-goals-mode proof-goals-mode
   "PhoX goals" nil
-  (setq 
-   proof-goals-font-lock-keywords 
-   (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
+  (setq  
+   font-lock-keywords phox-font-lock-keywords
    proof-output-fontify-enable     t)
   (phox-sym-lock-start)
   (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
@@ -234,6 +232,25 @@
   (append phox-top-keywords phox-proof-keywords)
 )
 
+;;;
+;;; X-Symbol
+;;;
+
+(defpgdefault x-symbol-language 'phox)
+
+;; (eval-after-load "x-symbol-phox"
+;;  ;; Add x-symbol tokens to phox-completion-table and rebuild
+;;  ;; internal completion table if completion is already active
+;; '(progn
+;;    (defpgdefault completion-table
+;;      (append (proof-ass completion-table)
+;; 	     (mapcar (lambda (xsym) (nth 2 xsym))
+;; 		     x-symbol-phox-table)))
+;;    (setq proof-xsym-font-lock-keywords
+;; 	 x-symbol-phox-font-lock-keywords)
+;;    (if (featurep 'completion)
+;;        (proof-add-completions))))
+
 (provide 'phox)