Various changes for win32 compatibility

5 files changed, 76 insertions, 42 deletions

diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index e4519b4c..c83fdef5 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -16,7 +16,8 @@
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-splash-time 4
+; timeout too long on win32. Why ?
+(defcustom proof-splash-time (if proof-running-on-win32 1 4)
   "Minimum number of seconds to display splash screen for.
 The splash screen may be displayed for a couple of seconds longer than
 this, depending on how long it takes the machine to initialise 
@@ -132,9 +133,12 @@ Borrowed from startup-center-spaces."
 	(progn
 	  (if (get-buffer-window splashbuf)
 	      ;; Restore the window config if splash is being displayed
-	      (set-window-configuration conf))
-	  ;; Destroy splash buffer 
-	  (kill-buffer splashbuf)))))
+	      (progn
+		;; Destroy buffer before restoring !
+		(kill-buffer splashbuf)
+		(set-window-configuration conf)
+		(redraw-device nil t))
+	    (kill-buffer splashbuf))))))
 
 (defvar proof-splash-seen nil
   "Flag indicating the user has been subjected to a welcome message.")
@@ -179,7 +183,7 @@ Borrowed from startup-center-spaces."
 	  (sit-for 0))
 	(setq proof-splash-timeout-conf
 	      (cons
-	       (add-timeout (if timeout proof-splash-time 20)
+	       (add-timeout (if timeout proof-splash-time 10)
 			    'proof-splash-remove-screen
 			    winconf)
 	       winconf)))
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 17b62992..6b3a92db 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -63,6 +63,8 @@
 (defun proof-toolbar-enabler (token)
   (intern (concat "proof-toolbar-" (symbol-name token) "-enable-p")))
 
+(defun proof-toolbar-function-with-enabler (token)
+  (intern (concat "proof-toolbar-" (symbol-name token) "-with-enabler-p")))
 
 ;;
 ;; Now the toolbar icons and buttons
@@ -105,13 +107,17 @@ and chooses the best one for the display properites.")
        (enabler	      (proof-toolbar-enabler token))
        (enableritem   (if enablep (list enabler) t))
        (buttonfn      (proof-toolbar-function token))
+       (buttonfnwe    (proof-toolbar-function-with-enabler token))
        (icon	      (proof-toolbar-icon token))
        (actualfn      (if (or enablep (not existsenabler))
 			  buttonfn
 			;; Add the enabler onto the function if necessary.
-			`(lambda ()
-				   (if (,enabler) 
-				       (call-interactively (quote ,buttonfn)))))))
+			(eval `(defun ,buttonfnwe ()
+				 (interactive)
+				 (if (,enabler) 
+				     (,buttonfn)
+				   (message ,(concat "Button \"" menuname "\" disabled")))))
+			buttonfnwe)))
     (if tooltip
 	(list (vector icon actualfn enableritem tooltip)))))
 
@@ -206,21 +212,27 @@ to the default toolbar."
   "Set flag to indicate that the toolbar should be refreshed."
   (setq proof-toolbar-refresh-flag t))
 
+(defvar proof-toolbar-enablers
+   (mapcar (lambda (tle) (list (proof-toolbar-enabler (car tle)))) (proof-ass toolbar-entries))
+  "List of all toolbar's enablers")
+
+(defvar proof-toolbar-enablers-last-state
+  nil
+  "Last state of the toolbar's enablers")
+
 (defun proof-toolbar-really-refresh (buf)
   "Force refresh of toolbar display to re-evaluate enablers.
 This function needs to be called anytime that enablers may have 
 changed state."
-  ;; FIXME: could improve performance here and reduce flickeryness
-  ;; by caching result of last evaluation of enablers.  If nothing
-  ;; has changed, don't remove and re-add.
   (if ;; Be careful to only add to correct buffer, and if it's live
-      (buffer-live-p buf)
-      ;; I'm not sure if this is "the" official way to do this,
-      ;; but it's what VM does and it works.
-      (progn
-	(remove-specifier default-toolbar buf)
-	(set-specifier default-toolbar proof-toolbar buf)
-	(setq proof-toolbar-refresh-flag nil))
+       (buffer-live-p buf)
+      (let ((enabler-state (mapcar 'eval proof-toolbar-enablers)))
+	(if 
+	    (not (equal enabler-state proof-toolbar-enablers-last-state))
+	    (progn
+	      (setq proof-toolbar-enablers-last-state enabler-state)
+	      (set-specifier-dirty-flag default-toolbar)
+	      (setq proof-toolbar-refresh-flag nil))))
     ;; Kill off this itimer if it's owning buffer has died
     (delete-itimer current-itimer)))
 
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"