From 802687cdbfaadc37d0c9682177ffc0597266e94c Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Tue, 1 Sep 2009 08:28:30 +0000 Subject: 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. --- phox/phox-fun.el | 6 +++--- phox/phox-lang.el | 28 ++++++++++++++++------------ phox/phox-pbrpm.el | 27 ++++++++++++++++++--------- phox/phox.el | 29 +++++++++++++++++++++++------ 4 files changed, 60 insertions(+), 30 deletions(-) (limited to 'phox') 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) -- cgit v1.2.3