various fixes.

.

3 files changed, 17 insertions, 93 deletions

diff --git a/af2/af2-font.el b/af2/af2-font.el
index 16ff42e9..c377ecc4 100644
--- a/af2/af2-font.el
+++ b/af2/af2-font.el
@@ -107,6 +107,8 @@
 ;;                       Sym-lock tables
 ;;--------------------------------------------------------------------------;;
 
+(if proof-running-on-XEmacs (require 'sym-lock))
+
 ;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
 ;; used to determine the symbol character codes.
 (defvar af2-sym-lock-keywords
diff --git a/af2/af2-fun.el b/af2/af2-fun.el
index 3560c7fc..8e253232 100644
--- a/af2/af2-fun.el
+++ b/af2/af2-fun.el
@@ -26,55 +26,10 @@ send a compile command to af2 for the theorem which name is under the cursor."
 
 (setq
  af2-forget-id-command "del %s.\n"
- af2-sy-definition-regexp "^[ \t\n\r]*\\(Cst\\|def\\)[ \t\n\r]*\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]*\"\\([^\"]*\\)\\)" 
- af2-definition-regexp "^[ \t\n\r]*\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]*\\([^ =\\[]*\\)"
+ af2-sy-definition-regexp "^[ \t\n\r]*\\(Cst\\|def\\)[ \t\n\r]+\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)" 
+ af2-definition-regexp "\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]+\\([^ =\\[]+\\)"
 )
 
-(defun string-search (sstr str &optional ipos)
-  (if str 
-      (let 
-	  ((pos (if ipos ipos 0)) (len (length sstr)) (end (- (length str) (length sstr))))
-	(if (not pos) (setq pos 0))
-	(while (and (<= pos end) 
-		    (not (string= sstr (substring str pos (+ pos len))))) 
-	  (setq pos (+ pos 1)))
-	(if (> pos end) nil pos)))) 
-
-(defun proof-remove-comment (str)
-  (if str (let 
-	      ((astr "")
-	       (pos 0)
-	       (lpos 0)
-	       (spos -1)
-               (epos -1)
-	       (lvl 0))
-	    (while (or spos epos)
-	      (setq
-	       spos (if (and spos (< spos lpos)) 
-			(string-search proof-comment-start str lpos) spos)
-	       epos (if (and epos (< epos lpos)) 
-			(string-search proof-comment-end str lpos) epos))
-	      (message (format "pos: %d, spos: %d, epos: %d, astr: %s ///" 
-			       pos (if spos spos -1) (if epos epos -1) astr))
-	      (if (and spos (or (not epos) (< spos epos)))
-		  (progn
-		    (if (= lvl 0) (setq astr 
-					(concat astr 
-						(substring str pos spos))))
-	  (setq lpos (+ spos 1) lvl (+ lvl 1)))
-		(if (and epos (> lvl 0)) 
-		    (progn
-		      (setq lpos (+ epos 1) lvl (- lvl 1))
-		      (if (= lvl 0) (setq pos (+ epos 2)))))))
-	    (setq astr (concat astr (substring str pos)))
-	    (message astr)
-	    astr)))
-
-;(defun proof-string-match-ignore-comments (regexp str matchpos)
-;  (let 
-;      (pos (proof-string-match regexp (proof-remove-comment str)))
-;    (if pos (string-match matchpos str) nil)))
-
 (defun af2-find-and-forget (span)
   (let (str ans tmp)
     (while span
@@ -84,22 +39,17 @@ send a compile command to af2 for the theorem which name is under the cursor."
        ((eq (span-property span 'type) 'comment))       
 
        ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat ans
-			  (format af2-forget-id-command
-				  (span-property span 'name)))))
+	(setq ans (concat (format af2-forget-id-command
+				  (span-property span 'name)) ans)))
 
        ((proof-string-match af2-sy-definition-regexp str)
-	(message "sy-definition:")
-	(message tmp)
 	(setq ans 
-	      (concat ans (format af2-forget-id-command 
-				  (concat "$" (match-string 4 str))))))
+	      (concat (format af2-forget-id-command 
+				  (concat "$" (match-string 4 str))) ans)))
 
        ((proof-string-match af2-definition-regexp str)
-	(message "definition:")
-	(message tmp)
-	(setq ans (concat ans (format af2-forget-id-command 
-				      (match-string 2 str))))))
+	(setq ans (concat (format af2-forget-id-command 
+				      (match-string 2 str)) ans))))
 
 
       (setq span (next-span span 'type)))
@@ -132,28 +82,4 @@ send a delete command to af2 for the symbol whose name is under the cursor."
     (if (char-equal (char-after (- end 1)) ?.)(setq end (- end 1)))
     (af2-delete-symbol (buffer-substring start end))))
 
-;; retract current goal
-
-(defun proof-retract-current-goal ()
-  "Retract the current proof, and move point to its start."
-  (interactive)
-  (proof-maybe-save-point
-   (let
-      ((span (proof-last-goal-or-goalsave)))
-     (if (and span (not (eq (span-property span 'type) 'goalsave))
-	      (< (span-end span) (proof-unprocessed-begin)))
-	 (progn
-	   (goto-char (span-start span))
-	   (proof-retract-until-point-interactive)
-	   (proof-maybe-follow-locked-end))
-       (error "Not proving")))))
-
-(require 'proof-script)
-
-(proof-define-assistant-command-witharg proof-find-string-in-names
-  "Search for items containing a given string in their names."
-   proof-find-string-in-names-command
-   "Find item with name containing"
- (proof-shell-invisible-command arg))
-
 (provide 'af2-fun)
\ No newline at end of file
diff --git a/af2/af2.el b/af2/af2.el
index 895b9096..e9924d0e 100644
--- a/af2/af2.el
+++ b/af2/af2.el
@@ -1,12 +1,10 @@
 (require 'proof)			; load generic parts
-(require 'sym-lock)
-
 
 ;; Adjust toolbar entries.  (Must be done
 ;; before proof-toolbar is loaded).
 
-(setq af2-toolbar-entries
-      (remassoc 'context af2-toolbar-entries))
+(if proof-running-on-XEmacs (setq af2-toolbar-entries
+      (remassoc 'context af2-toolbar-entries)))
 
 
 ;; ======== User settings for Af2 ========
@@ -113,10 +111,10 @@
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    proof-state-command             "goals."
-   proof-goal-command-regexp       "^[ \n\t\r]*goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
-   proof-save-command-regexp       "^[ \n\t\r]*save"
-   proof-goal-with-hole-regexp     "^[ \n\t\r]*\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)[ \n\t\r]*\\([^ \n\t\r]*\\)"
-   proof-save-with-hole-regexp     "^[ \n\t\r]*save[ \n\t\r]*\\(\\([^ \n\t\r]*\\)\\)"
+   proof-goal-command-regexp       "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
+   proof-save-command-regexp       "save"
+   proof-goal-with-hole-regexp     "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)[ \n\t\r]+\\([^ \n\t\r]+\\)"
+   proof-save-with-hole-regexp     "save[ \n\t\r]+\\(\\([^ \n\t\r]+\\)\\)[ \n\t\r]*\.[ \n\t\r]"
    proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
    proof-non-undoables-regexp      "undo"
    proof-goal-command              "goal %s."
@@ -125,7 +123,7 @@
    proof-showproof-command         "goals."
    proof-undo-n-times-cmd          "undo %s."
    proof-find-and-forget-fn        'af2-find-and-forget
-   proof-find-string-in-names-command      "search \"%s\"."
+   proof-find-theorems-command      "search \"%s\"."
    proof-auto-multiple-files       nil
    font-lock-keywords              af2-font-lock-keywords 
    )
@@ -165,8 +163,6 @@
       'proof-assert-next-command-interactive)
     (define-key af2-mode-map [(control c) (meta d)] 
       'af2-delete-symbol-around-point)  
-;    (defalias 'proof-toolbar-retract 'proof-retract-current-goal)
-    (defalias 'proof-toolbar-find 'proof-find-string-in-names)
     ;; Configure syntax table for block comments
     (modify-syntax-entry ?\* ". 23")
     (modify-syntax-entry ?\( "()1")