*** empty log message ***

2 files changed, 20 insertions, 15 deletions

diff --git a/af2/sym-lock.el b/af2/sym-lock.el
index 3f9807e6..085ef268 100644
--- a/af2/sym-lock.el
+++ b/af2/sym-lock.el
@@ -107,27 +107,32 @@
   (let ((num (if (fboundp 'face-height)
 		 (face-height 'default)
 	       (let ((str (face-font 'default)))
-		 (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*" str)
-		 (string-to-number (substring str (match-beginning 1)
-					      (match-end 1))))))
+		 (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--*")))
     (while (and lf maxsize)
-      (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*"
+      (if 
+	  (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*"
 		    (car lf))
-      (setq size (string-to-number (substring (car lf) (match-beginning 1)
-					      (match-end 1))))
-      (if (and (> size num) (< size maxsize))
-	  (setq maxsize nil)
-	(setq oldsize size))
+	  (progn 
+	    (setq size (string-to-number (substring (car lf) (match-beginning 1)
+						    (match-end 1))))
+	    (if (and (> size num) (< size maxsize))
+		(setq maxsize nil)
+	      (setq oldsize size))))
       (setq lf (cdr lf)))
     (number-to-string (if (and oldsize (< oldsize 100)) oldsize num))))
 
 (defvar sym-lock-font-name
-  (concat "-adobe-symbol-medium-r-normal--"
-	  (if sym-lock-font-size sym-lock-font-size
-	    (sym-lock-compute-font-size))
-	  "-*-*-*-p-*-adobe-fontspecific")
+  (if window-system
+      (concat "-adobe-symbol-medium-r-normal--"
+	      (if sym-lock-font-size sym-lock-font-size
+		(sym-lock-compute-font-size))
+	      "-*-*-*-p-*-adobe-fontspecific")
+    "")
   "Name of the font used by Sym-Lock.")
 (make-variable-buffer-local 'sym-lock-font-name)
 (put 'sym-lock-font-name 'permanent-local t)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 2e5ce9d0..7bd11e91 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -369,7 +369,7 @@ directory and elisp file for the mode, which will be
 where @samp{PROOF-HOME-DIRECTORY} is the value of the
 variable @code{proof-home-directory}.
 
-The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (af2 "Af2" "\\.af2$") (hol98 "HOL" "\\.sml$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}.
+The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (af2 "Af2" "\\.af2$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}.
 @end defopt
 
 
@@ -2445,7 +2445,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'af2} @code{'hol98} @code{'plastic} @code{'twelf}.
+A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'af2} @code{'hol98} @code{'acl2} @code{'plastic} @code{'twelf}.
 Each proof assistant defines its own instance of Proof General,
 providing session control, script management, etc.  Proof General
 will be started automatically for the assistants chosen here.