major modifications including outline, atgs, ...

1 files changed, 34 insertions, 265 deletions

diff --git a/af2/af2.el b/af2/af2.el
index e36f6058..895b9096 100644
--- a/af2/af2.el
+++ b/af2/af2.el
@@ -1,11 +1,13 @@
 (require 'proof)			; load generic parts
 (require 'sym-lock)
 
+
 ;; Adjust toolbar entries.  (Must be done
 ;; before proof-toolbar is loaded).
 
 (setq af2-toolbar-entries
-      (remassoc 'state af2-toolbar-entries))
+      (remassoc 'context af2-toolbar-entries))
+
 
 ;; ======== User settings for Af2 ========
 ;;
@@ -65,152 +67,16 @@
   :type 'boolean
   :group 'af2-config)
 
+(defcustom af2-etags 
+  (concat af2-doc-dir "/tools/af2_etags.sh")
+  "Command to build tags table."
+  :type 'string
+  :group 'af2-config)
 
-
-
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                         gestion des TAGS
-;;--------------------------------------------------------------------------;;
-
-; sous xemacs, visit-tags-table n'a pas d'argument optionnel. Sous gnu emacs :
-
-; Normally M-x visit-tags-table sets the global value of `tags-file-name'.
-; With a prefix arg, set the buffer-local value instead.
-
-; mieux vaut sous gnu emacs gérer la variable tags-table-list, qui
-; n'existe pas sous xemacs.
-; Sous xemacs il faut gérer la variable tag-table-alist qui n'existe pas
-; sous gnu emacs.
-
-;(defun af2-tags-load-table(table)
-;  "load tags table"
-;  (interactive "D directory, location of a file named TAGS to load : ")
-;  (visit-tags-table table 4)
-;  )
-
-;(defun af2-tags-doc-table()
-;  "tags in text documentation"
-;  (interactive)
-;  (visit-tags-table (concat af2-doc-dir "/text/") 4)
-;  )
-
-;(defun af2-tags-lib-table()
-;  "tags in libraries"
-;  (interactive)
-;  (visit-tags-table af2-lib-dir 4)
-;  )
-
-
-
-(defun af2-tags-add-table(table)
-  "add tags table"
-  (interactive "D directory, location of a file named TAGS to add : ")
-  (if proof-running-on-XEmacs
-      (let ((association (cons buffer-file-name table)))
-	(if (member association tag-table-alist)
-	    (message (concat table " already loaded."))
-	  (setq tag-table-alist (cons association tag-table-alist))))
-; gnu emacs
-    (if (member table tags-table-list)
-	(message (concat table " already loaded."))
-;    (make-local-variable 'tags-table-list) ; ne focntionne pas
-      (setq tags-table-list (cons table tags-table-list))
-      )
-    )
-  )
-
-(defun af2-tags-reset-table()
-  "Set tags-table-list to nil."
-  (interactive)
-;  (make-local-variable 'tags-table-list)
-  (if proof-running-on-XEmacs
-      (setq tag-table-alist (remassoc buffer-file-name tag-table-alist))
-    (setq tags-table-list nil))
-  )
-
-(defun af2-tags-add-doc-table()
-  "Add tags in text documentation."
-  (interactive)
-  (af2-tags-add-table (concat af2-doc-dir "/text/TAGS"))
-  )
-
-(defun af2-tags-add-lib-table()
-  "Add tags in libraries."
-  (interactive)
-  (af2-tags-add-table (concat af2-lib-dir "TAGS"))
-  )
- 
-(defun af2-tags-add-local-table()
-  "Add the tags table created with function af2-create-local-table."
-  (interactive)
-  (af2-tags-add-table (concat buffer-file-name "TAGS"))
-  )
-
-(defun af2-tags-create-local-table()
-  "create table on local buffer"
-  (interactive)
-  (shell-command (concat af2-etags 
-			 " -o " 
-			 (file-name-nondirectory (buffer-file-name))
-			 "TAGS "
-			 (file-name-nondirectory (buffer-file-name))))
-  )
-
-;; default
-
-(if af2-tags-doc (add-hook 'af2-mode-hook 'af2-tags-add-doc-table))
-
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;; program extraction.
-;;
-;; note : program extraction is still experimental
-;;--------------------------------------------------------------------------;;
-
-(defun af2-compile-theorem(name)
-  "Interactive function : 
-ask for the name of a theorem and send a compile command to af2 for it."
-  (interactive "stheorem : ")
-  (proof-shell-invisible-command (concat "compile " name ".\n")))
-
-(defun af2-compile-theorem-around-point()
-"Interactive function : 
-send a compile command to af2 for the theorem which name is under the cursor."
-  (interactive)
-  (let (start end)
-    (save-excursion
-      (forward-word 1)
-      (setq start (point))
-      (forward-word -1)
-      (setq end (point)))
-    (af2-compile-theorem (buffer-substring start end))))
-
-;;--------------------------------------------------------------------------;;
-;;
-;;    Deleting symbols
-;;
-;;--------------------------------------------------------------------------;;
-
-
-(defun af2-delete-symbol(symbol)
-  "Interactive function : 
-ask for a symbol and send a delete command to af2 for it."
-  (interactive "ssymbol : ")
-  (proof-shell-invisible-command (concat "del " symbol ".\n")))
-
-(defun af2-delete-symbol-around-point()
-"Interactive function : 
-send a delete command to af2 for the symbol whose name is under the cursor."
-  (interactive)
-  (let (start end)
-    (save-excursion
-      (forward-word -1)
-      (setq start (point))
-      (forward-word 1)
-      (setq end (point)))
-    (if (char-equal (char-after (- end 1)) ?.)(setq end (- end 1)))
-    (af2-delete-symbol (buffer-substring start end))))
+(require 'af2-tags)
+(require 'af2-outline)
+(require 'af2-font)
+(require 'af2-fun)
 
 ;; ----- Af2 specific menu
 
@@ -238,136 +104,32 @@ send a delete command to af2 for the symbol whose name is under the cursor."
 ;;
 ;; ======== Configuration of generic modes ========
 ;;
-(defconst af2-font-lock-keywords
-  (list
-;commands
-   '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)"
-    0 'font-lock-comment-face t)
-   '("\"\\([^\\\"]\\|\\\\.\\)*\""
-    0 'font-lock-string-face t)
-    (cons (concat "\\([ \t]\\|^\\)\\("
-       "\\(Cst\\)\\|"
-       "\\(Import\\)\\|"
-       "\\(Use\\)\\|"
-       "\\(Sort\\)\\|"
-       "\\(new_\\(\\(intro\\)\\|\\(elim\\)\\|\\(rewrite\\)\\)\\)\\|"
-       "\\(a\\("
-       (concat
-	"\\(dd_path\\)\\|"
-	"\\(uthor\\)"
-	"\\)\\)\\|")
-       "\\(c\\("
-       (concat
-	"\\(laim\\)\\|"
-	"\\(ose_def\\)"
-	"\\)\\)\\|")
-       "\\(d\\(\\(e\\(f\\|l\\)\\)\\|\\(ocuments\\)\\|\\(epend\\)\\)\\)\\|"
-       "\\(e\\("
-       (concat 
-	"\\(lim_after_intro\\)\\|"
-	"\\(xport\\)\\|"
-	"\\(del\\)\\|"
-	"\\(show\\)"
-	"\\)\\)\\|")
-       "\\(flag\\)\\|"
-       "\\(goal\\)\\|"
-       "\\(in\\("
-       (concat
-	"\\(clude\\)\\|"
-	"\\(stitute\\)"
-	"\\)\\)\\|")
-       "\\(p\\(\\(ath\\)\\|\\(r\\(\\(int_sort\\)\\|\\(iority\\)\\)\\)\\)\\)\\|"
-       "\\(quit\\)\\|"
-       "\\(s\\(\\(ave\\)\\|\\(earch\\)\\)\\)\\|"
-       "\\(t\\(" 
-       (concat
-	"\\(ex\\(_syntax\\)?\\)\\|"
-	"\\(itle\\)"
-	"\\)\\)")
-       "\\)[ \t.]")
-      '(0 'font-lock-keyword-face t))
-;proof command
-    (cons (concat "\\([ \t]\\|^\\)\\("
-       "\\(a\\("
-       (concat
-	"\\(bort\\)\\|"
-	"\\(bsurd\\)\\|"
-	"\\(pply\\)\\|"
-	"\\(xiom\\)"
-	"\\)\\)\\|")
-       "\\(constraints\\)\\|"
-       "\\(elim\\)\\|"
-       "\\(from\\)\\|"
-       "\\(goals\\)\\|"
-       "\\(in\\("
-       (concat
-	"\\(tros?\\)\\|"
-	"\\(stance\\)"
-	"\\)\\)\\|")
-       "\\(l\\("
-       (concat
-	"\\(ocal\\)\\|"
-	"\\(efts?\\)"
-	"\\)\\)\\|")
-       "\\(next\\)\\|"
-       "\\(r\\(\\(ewrite\\(_hyp\\)?\\)\\|\\(ename\\)\\|\\(mh\\)\\)\\)\\|"
-       "\\(slh\\)\\|"
-       "\\(trivial\\)\\|" 
-       "\\(u\\("       
-       (concat
-	"\\(se\\)\\|"
-	"\\(ndo\\)\\|"
-	"\\(nfold\\(_hyp\\)?\\)\\)\\)") 
-       "\\)[ \t.]")
-      '(0 'font-lock-type-face t))))
-
-;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
-;; used to determine the symbol character codes.
-(defvar af2-sym-lock-keywords
-  '((">=" 0 1 179)
-    ("<=" 0 1 163)
-    ("!=" 0 1 185)
-    (":<" 0 1 206)
-    ("[^:]\\(:\\)[^:=]" 1 7 206)
-    ("\\\\/" 0 1 36)
-    ("/\\\\" 0 1 34)
-    ("\\<or\\>" 0 3 218) 
-    ("&" 0 1 217) 
-    ("<->" 0 1 171)
-    ("-->" 0 1 222)
-    ("->" 0 1 174)
-    ("~" 0 1 216))
-  "If non nil: Overrides default Sym-Lock patterns for Af2.")
-
-(defun af2-sym-lock-start ()
-	(if (and (featurep 'sym-lock) af2-sym-lock)
-	    (progn
-	      (setq sym-lock-color
-		    (face-foreground 'font-lock-function-name-face))
-	      (if (not sym-lock-keywords)
-		  (sym-lock af2-sym-lock-keywords)))))
 
 (defun af2-config ()
   "Configure Proof General scripting for Af2."
   (setq
    proof-terminal-char		?\.	; ends every command
-   proof-script-command-end-regexp "[.]\\($\\| \\)"
+   proof-script-command-end-regexp "[.][ \n\t\r]"
    proof-comment-start             "(*"
    proof-comment-end               "*)"
-   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\\) \\([^ ]*\\)"
-   proof-save-with-hole-regexp     "save \\(\\([^ ]*\\)\\)"
-   proof-shell-error-regexp        "^\\([^ ]* \\)?\\(e\\|E\\)rror"
+   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-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
    proof-non-undoables-regexp      "undo"
    proof-goal-command              "goal %s."
    proof-save-command              "save %s."
    proof-kill-goal-command         "abort."
    proof-showproof-command         "goals."
    proof-undo-n-times-cmd          "undo %s."
-   proof-auto-multiple-files       t
+   proof-find-and-forget-fn        'af2-find-and-forget
+   proof-find-string-in-names-command      "search \"%s\"."
+   proof-auto-multiple-files       nil
    font-lock-keywords              af2-font-lock-keywords 
- ))
+   )
+)
 
 (defun af2-shell-config ()
   "Configure Proof General shell for Af2."
@@ -376,15 +138,13 @@ send a delete command to af2 for the symbol whose name is under the cursor."
    proof-shell-prompt-pattern      "\\(>af2> \\)\\|\\(%af2% \\)"
    proof-shell-annotated-prompt-regexp  "\\(>af2> \\)\\|\\(%af2% \\)"
    proof-shell-interrupt-regexp    "Interrupt"
-   proof-shell-start-goals-regexp  "^START GOALS"
-   proof-shell-end-goals-regexp    "^END GOALS"
+   proof-shell-start-goals-regexp  "^Goals left to prove:"
    proof-shell-quit-cmd            "quit."
    proof-shell-restart-cmd         "quit."
    proof-shell-proof-completed-regexp   "^.*^proved"
 ))
 
 
-
 ;;
 ;; ======== Defining the derived modes ========
 ;;
@@ -400,6 +160,13 @@ send a delete command to af2 for the symbol whose name is under the cursor."
     (af2-config)
     (af2-sym-lock-start)
     (proof-config-done)
+    (af2-setup-outline)
+    (define-key af2-mode-map [(control j)] 
+      '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")
@@ -441,3 +208,5 @@ send a delete command to af2 for the symbol whose name is under the cursor."
   (setq proof-mode-for-pbp	'af2-goals-mode))
 
 (provide 'af2)
+
+