aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2001-07-25 14:15:34 +0000
committerGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2001-07-25 14:15:34 +0000
commit4b511ab973f04e878dfb4288ba6006871b467eb8 (patch)
treea922c9687092bb18ae82b4e321198cfece936296 /phox
parentd566389017383722af7f3390569cd51f96325fee (diff)
Various changes for win32 compatibility
Diffstat (limited to 'phox')
-rw-r--r--phox/phox-fun.el1
-rw-r--r--phox/phox-sym-lock.el62
-rw-r--r--phox/phox.el3
3 files changed, 42 insertions, 24 deletions
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 6cf8fc4b..22d3e717 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -240,7 +240,6 @@ or for optional argument TABLE."
"Process until the end of the next unprocessed command after point.
If inside a comment, just process until the start of the comment."
(interactive)
- (message "test")
(if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
(proof-with-script-buffer
(proof-maybe-save-point
diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el
index 4db08bde..efee6088 100644
--- a/phox/phox-sym-lock.el
+++ b/phox/phox-sym-lock.el
@@ -108,34 +108,52 @@
(defun phox-sym-lock-compute-font-size ()
"Computes the size of the \"better\" symbol font."
- (let ((num (if (fboundp 'face-height)
- (face-height 'default)
- (let ((str (face-font 'default)))
- (if
- (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*" str)
- (string-to-number (substring str (match-beginning 1)
- (match-end 1)))))))
- (maxsize 100) (size) (oldsize)
- (lf (list-fonts "-adobe-symbol-medium-r-normal--*")))
+ (let ((font-reg (if proof-running-on-win32
+ "[^:]*:[^:]*:\\([^:]*\\):[^:]*:[^:]*"
+ "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*"))
+ (font-pat (if proof-running-on-win32
+ "Symbol:Regular:*::Symbol"
+ "-adobe-symbol-medium-r-normal--*")))
+ (let (
+; face-height is not very good on win32. Why ?
+ (num (if (and (not proof-running-on-win32) (fboundp 'face-height))
+ (face-height 'default)
+ (let ((str (face-font-name 'default)))
+ (if
+ (string-match font-reg str)
+ (string-to-number (substring str (match-beginning 1)
+ (match-end 1)))))))
+ (maxsize 100) (size) (oldsize)
+ (lf (list-fonts font-pat)))
(while (and lf maxsize)
(if
- (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*"
+ (string-match font-reg
(car lf))
- (progn
- (setq size (string-to-number (substring (car lf) (match-beginning 1)
+ (let ((str-size (substring (car lf) (match-beginning 1)
(match-end 1))))
- (if (and (> size num) (< size maxsize))
- (setq maxsize nil)
- (setq oldsize size))))
+ ; test for variable size fonts. Hope it is generic ?
+ (if (or (equal str-size "*")(equal str-size ""))
+ (progn
+ (setq oldsize num)
+ (setq lf nil))
+ (setq size (string-to-number str-size))
+ (if (and (> size num) (< size maxsize))
+ (setq lf nil)
+ (setq oldsize size)))))
(setq lf (cdr lf)))
- (number-to-string (if (and oldsize (< oldsize 100)) oldsize num))))
+ (number-to-string (if (and oldsize (< oldsize maxsize)) oldsize num)))))
(defvar phox-sym-lock-font-name
(if window-system
- (concat "-adobe-symbol-medium-r-normal--"
- (if phox-sym-lock-font-size phox-sym-lock-font-size
- (phox-sym-lock-compute-font-size))
- "-*-*-*-p-*-adobe-fontspecific")
+ (if proof-running-on-win32
+ (concat "Symbol:Regular:"
+ (if phox-sym-lock-font-size phox-sym-lock-font-size
+ (phox-sym-lock-compute-font-size))
+ "::Symbol")
+ (concat "-adobe-symbol-medium-r-normal--"
+ (if phox-sym-lock-font-size phox-sym-lock-font-size
+ (phox-sym-lock-compute-font-size))
+ "-*-*-*-p-*-adobe-fontspecific"))
"")
"Name of the font used by Phox-Sym-Lock.")
(make-variable-buffer-local 'phox-sym-lock-font-name)
@@ -159,7 +177,7 @@
(set-face-property 'phox-sym-lock-adobe-symbol-face
'font phox-sym-lock-font-name nil
'(mule-fonts) 'prepend))
- (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name))
+ (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global))
(defun phox-sym-lock-set-foreground ()
"Set foreground color of Phox-Sym-Lock faces."
@@ -248,7 +266,7 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic.
(setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent)
phox-sym-lock-ext-end (extent-end-position font-lock-old-extent))
(setq phox-sym-lock-ext-start nil))
- (error (warn "Error caught in `phox-sym-lock-pre-idle-hook-first'"))))
+ (error (setq phox-sym-lock-ext-start nil))))
(defun phox-sym-lock-pre-idle-hook-last ()
(condition-case nil
diff --git a/phox/phox.el b/phox/phox.el
index 12d4e305..2f0680e9 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -147,7 +147,8 @@
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]* goals? created\\)"
+ proof-shell-end-goals-regexp "^End of goals."
proof-shell-quit-cmd "quit."
proof-shell-restart-cmd "restart."
proof-shell-proof-completed-regexp "^.*^proved"