*** empty log message ***

3 files changed, 14 insertions, 14 deletions

diff --git a/af2/sym-lock.el b/af2/sym-lock.el
index 78e3c82f..3f9807e6 100644
--- a/af2/sym-lock.el
+++ b/af2/sym-lock.el
@@ -262,6 +262,11 @@ OBJ under `sym-lock-adobe-symbol-face'. The face extent will become atomic."
   "Function called by `font-lock-mode' for initialization purposes."
   (add-hook 'pre-idle-hook 'sym-lock-pre-idle-hook-first)
   (add-hook 'pre-idle-hook 'sym-lock-pre-idle-hook-last t)
+  (add-menu-button '("Options" "Syntax Highlighting")
+		   ["Sym-Lock"
+		    (if sym-lock-enabled (sym-lock-disable) (sym-lock-enable))
+		    :style toggle :selected sym-lock-enabled
+		    :active sym-lock-keywords] "Automatic")  
   (if (and (featurep 'sym-lock) sym-lock-enabled
 	   font-lock-defaults (boundp 'sym-lock-keywords))
       (progn
@@ -294,12 +299,6 @@ OBJ under `sym-lock-adobe-symbol-face'. The face extent will become atomic."
       (setq font-lock-keywords (append sym-lock-keywords
 				       font-lock-keywords))) t)
 
-(add-menu-button '("Options" "Syntax Highlighting")
-		 ["Sym-Lock"
-		  (if sym-lock-enabled (sym-lock-disable) (sym-lock-enable))
-		  :style toggle :selected sym-lock-enabled
-		  :active sym-lock-keywords] "Automatic")
-
 (add-hook 'font-lock-mode-hook 'sym-lock-font-lock-hook)
 
 (provide 'sym-lock)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 057d4ad7..2e5ce9d0 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -108,7 +108,7 @@ END-INFO-DIR-ENTRY
 @c so we take it out for now.
 @c Ideally would like some way of generating eps from
 @c the .jpg file.   
-@image{ProofGeneralPortrait}
+@c image{ProofGeneralPortrait}
 @end ifset
 @end iftex
 @author David Aspinall with T. Kleymann
@@ -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$") (acl2 "ACL2" "\\.acl2$") (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$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}.
 @end defopt
 
 
@@ -828,7 +828,9 @@ for @samp{@code{proof-script-next-entity-regexps}} used for function menus.
 @c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp
 @defvar proof-goal-with-hole-regexp 
 Regexp which matches a command used to issue and name a goal.@*
-Match number 2 should be the name of the goal issued.
+The name of the theorem is build from the variable
+@code{proof-goal-with-hole-result} using the same convention as 
+@code{query-replace-regexp}. 
 Used for setting names of goal..save regions and for default
 @code{function-menu} configuration in @code{proof-script-find-next-entity}.
 
@@ -854,7 +856,9 @@ Matches a save command.
 @c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp
 @defvar proof-save-with-hole-regexp 
 Regexp which matches a command to save a named theorem.@*
-Match number 2 should be the name of the theorem saved.
+The name of the theorem is build from the variable
+@code{proof-save-with-hole-result} using the same convention as 
+@code{query-replace-regexp}. 
 Used for setting names of goal..save regions and for default
 @code{function-menu} configuration in @code{proof-script-find-next-entity}.
 
@@ -2441,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{'acl2} @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{'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.
diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el
index 7673ee89..5550f324 100644
--- a/doc/docstring-magic.el
+++ b/doc/docstring-magic.el
@@ -15,9 +15,6 @@
 (require 'proof-compat)
 (require 'proof-utils)
 
-
-(provide 'sym-lock) ;  Hack for af2: sym-lock gives error when loaded, why?
-
 ;; FIXME: Loading several prover files at once is a bit of a problem
 ;; with new config mechanism.
 ;; Could abstract more code in proof-site.el to avoid duplication here.