*** empty log message ***

3 files changed, 80 insertions, 8 deletions

diff --git a/af2/af2-font.el b/af2/af2-font.el
index c377ecc4..32586094 100644
--- a/af2/af2-font.el
+++ b/af2/af2-font.el
@@ -116,7 +116,7 @@
     ("<=" 0 1 163)
     ("!=" 0 1 185)
     (":<" 0 1 206)
-    ("[^:]\\(:\\)[^:=]" 1 7 206)
+    ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206)
     ("\\\\/" 0 1 36)
     ("/\\\\" 0 1 34)
     ("\\<or\\>" 0 3 218) 
diff --git a/af2/af2-fun.el b/af2/af2-fun.el
index ff442fbc..6a0a20cd 100644
--- a/af2/af2-fun.el
+++ b/af2/af2-fun.el
@@ -26,6 +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-forget-new-elim-command "edel elim %s.\n"
+ af2-forget-new-intro-command "edel intro %s.\n"
+ af2-forget-new-rewrite-command "edel rewrite %s.\n"
+ af2-forget-close-def-command "edel closed %s.\n"
  af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
  af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
  af2-spaces-regexp "[ \n\t\r]*"
@@ -37,6 +41,19 @@ send a compile command to af2 for the theorem which name is under the cursor."
    "\\(Cst\\|def\\|claim\\|Sort\\)"
    af2-comments-regexp
    af2-ident-regexp)
+ af2-new-elim-regexp (concat
+   "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
+   af2-ident-regexp)
+ af2-new-intro-regexp (concat
+   "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
+   af2-ident-regexp)
+ af2-new-rewrite-regexp (concat
+   "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
+   af2-ident-regexp)
+ af2-close-def-regexp (concat
+   "close_def"
+   af2-comments-regexp
+   "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
 )
 
 (defun af2-find-and-forget (span)
@@ -52,6 +69,26 @@ send a compile command to af2 for the theorem which name is under the cursor."
 	(setq ans (concat (format af2-forget-id-command
 				  (span-property span 'name)) ans)))
 
+       ((proof-string-match af2-new-elim-regexp str)
+	(setq ans 
+	      (concat (format af2-forget-new-elim-command 
+				  (match-string 3 str)) ans)))
+
+       ((proof-string-match af2-new-intro-regexp str)
+	(setq ans 
+	      (concat (format af2-forget-new-intro-command 
+				  (match-string 3 str)) ans)))
+
+       ((proof-string-match af2-new-rewrite-regexp str)
+	(setq ans 
+	      (concat (format af2-forget-new-rewrite-command 
+				  (match-string 3 str)) ans)))
+
+       ((proof-string-match af2-close-def-regexp str)
+	(setq ans 
+	      (concat (format af2-forget-close-def-command 
+				  (match-string 4 str)) ans)))
+
        ((proof-string-match af2-sy-definition-regexp str)
 	(setq ans 
 	      (concat (format af2-forget-id-command 
@@ -93,4 +130,26 @@ 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))))
 
-(provide 'af2-fun)
\ No newline at end of file
+;;
+;; Doing commands
+;;
+
+(defun af2-assert-next-command-interactive ()
+  "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 (or 
+       (and (= (point) (point-max)) (= (char-before (point)) ?.))
+       (and (not (proof-re-search-forward proof-script-command-end-regexp
+					  (point-max) t))
+	    (proof-re-search-forward "\\.\\'" (point-max) t)))
+       (insert "\n"))
+  (proof-with-script-buffer
+   (proof-maybe-save-point
+    (goto-char (proof-queue-or-locked-end))
+    (proof-assert-next-command))
+   (proof-maybe-follow-locked-end)))
+
+(provide 'af2-fun)
+
diff --git a/af2/af2.el b/af2/af2.el
index 10dd0573..505b4c39 100644
--- a/af2/af2.el
+++ b/af2/af2.el
@@ -107,7 +107,7 @@
   "Configure Proof General scripting for Af2."
   (setq
    proof-terminal-char		?\.	; ends every command
-   proof-script-command-end-regexp "[.]\\([ \t]\\|$\\)"
+   proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)"
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    proof-state-command             "goals."
@@ -117,6 +117,7 @@
       "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)"
       af2-comments-regexp
       af2-ident-regexp)
+   proof-non-undoables-regexp      "\\(constraints\\|flags\\|goals\\"
    proof-goal-with-hole-result     5
    proof-save-with-hole-regexp     (concat 
       "save"
@@ -168,7 +169,10 @@
     (proof-config-done)
     (af2-setup-outline)
     (define-key af2-mode-map [(control j)] 
-      'proof-assert-next-command-interactive)
+      'af2-assert-next-command-interactive)
+    ;; with the previous binding,
+    ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed"
+
     (define-key af2-mode-map [(control c) (meta d)] 
       'af2-delete-symbol-around-point)  
     ;; Configure syntax table for block comments
@@ -183,12 +187,21 @@
 
 (define-derived-mode af2-response-mode proof-response-mode
   "Af2 response" nil
-  (proof-response-config-done))
+  (setq 
+   font-lock-keywords  af2-font-lock-keywords
+   proof-output-fontify-enable     t)
+  (af2-sym-lock-start)
+  (proof-response-config-done)
+  (font-lock-mode))
 
-(define-derived-mode af2-goals-mode pbp-mode
+(define-derived-mode af2-goals-mode proof-goals-mode
   "Af2 goals" nil
+  (setq 
+   font-lock-keywords  af2-font-lock-keywords
+   proof-output-fontify-enable     t)
   (af2-sym-lock-start)
-  (proof-goals-config-done))
+  (proof-goals-config-done)
+  (font-lock-mode))
 
 ;; The response buffer and goals buffer modes defined above are
 ;; trivial.  In fact, we don't need to define them at all -- they
@@ -209,7 +222,7 @@
   (setq proof-prog-name		af2-prog-name)
   (setq proof-mode-for-shell    'af2-shell-mode)
   (setq proof-mode-for-response 'af2-response-mode)
-  (setq proof-mode-for-pbp	'af2-goals-mode))
+  (setq proof-mode-for-goals	'af2-goals-mode))
 
 (provide 'af2)