af2 is now called PhoX

8 files changed, 0 insertions, 988 deletions

diff --git a/af2/README b/af2/README
deleted file mode 100644
index 9c955b84..00000000
--- a/af2/README
+++ /dev/null
@@ -1,19 +0,0 @@
-PhoX Proof General, for Phox.
-
-Written by Christophe Raffalli
-
-$Id$
-
-Status:	       supported
-Maintainer:    Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
-PhoX version:  0.7
-PhoX homepage:  http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html
-
-========================================
-
-This mode has support for script management with PhoX, and some
-other features ported from PhoX's own Emacs mode.
-
-
-
-
diff --git a/af2/example.af2 b/af2/example.af2
deleted file mode 100644
index 36ece411..00000000
--- a/af2/example.af2
+++ /dev/null
@@ -1,9 +0,0 @@
-(*
-    Example proof script for AF2 Proof General
-
-    $Id$
-*)
-
-prop (* test *) (* just un test *) test /\X (X -> X).
-trivial.
-save.
\ No newline at end of file
diff --git a/af2/phox-font.el b/af2/phox-font.el
deleted file mode 100644
index f04844fa..00000000
--- a/af2/phox-font.el
+++ /dev/null
@@ -1,138 +0,0 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                       Font lock keywords
-;;--------------------------------------------------------------------------;;
-
-(defconst phox-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\\)\\|"
-	"\\(or\\(ollary\\)?\\)"
-	"\\)\\)\\|")
-       "\\(d\\(\\(e\\(f\\(_thlist\\)?\\|l\\)\\)\\|\\(ocuments\\)\\|\\(epend\\)\\)\\)\\|"
-       "\\(e\\("
-       (concat 
-	"\\(lim_after_intro\\)\\|"
-	"\\(xport\\)\\|"
-	"\\(del\\)\\|"
-	"\\(show\\)"
-	"\\)\\)\\|")
-       "\\(f\\("
-       (concat
-	"\\(act\\)\\|"
-	"\\(lag\\)\\|"
-	"\\)\\)\\|")
-       "\\(goal\\)\\|"
-       "\\(in\\("
-       (concat
-	"\\(clude\\)\\|"
-	"\\(stitute\\)"
-	"\\)\\)\\|")
-       "\\(lem\\(ma\\)?\\)\\|"
-       "\\(p\\("
-       (concat
-	"\\(ath\\)\\|"
-	"\\(r\\("
-	(concat
-	 "\\(int\\(_sort\\)?\\)\\|"
-	 "\\(iority\\)\\|"
-	 "\\(op\\(osition\\)?\\)"
-	 "\\)\\)")
-	"\\)\\)\\|")
-       "\\(quit\\)\\|"
-       "\\(s\\(\\(ave\\)\\|\\(earch\\)\\)\\)\\|"
-       "\\(t\\(" 
-       (concat
-	"\\(ex\\(_syntax\\)?\\)\\|"
-	"\\(eheo\\(rem\\)?\\)\\|"
-	"\\(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))))
-
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                       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 phox-sym-lock-keywords
-  '((">=" 0 1 179)
-    ("<=" 0 1 163)
-    ("!=" 0 1 185)
-    (":<" 0 1 206)
-    ("[^:]\\(:\\)[^:= \n\t\r]" 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 PhoX.")
-
-(defun phox-sym-lock-start ()
-	(if (and (featurep 'sym-lock) phox-sym-lock)
-	    (progn
-	      (setq sym-lock-color
-		    (face-foreground 'font-lock-function-name-face))
-	      (if (not sym-lock-keywords)
-		  (sym-lock phox-sym-lock-keywords)))))
-
-(provide 'phox-font)
diff --git a/af2/phox-fun.el b/af2/phox-fun.el
deleted file mode 100644
index 58771057..00000000
--- a/af2/phox-fun.el
+++ /dev/null
@@ -1,150 +0,0 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;; program extraction.
-;;
-;; note : program extraction is still experimental
-;;--------------------------------------------------------------------------;;
-
-(defun phox-compile-theorem(name)
-  "Interactive function : 
-ask for the name of a theorem and send a compile command to PhoX for it."
-  (interactive "stheorem : ")
-  (proof-shell-invisible-command (concat "compile " name ".\n")))
-
-(defun phox-compile-theorem-around-point()
-"Interactive function : 
-send a compile command to PhoX 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)))
-    (phox-compile-theorem (buffer-substring start end))))
-
-
-(setq
- phox-forget-id-command "del %s.\n"
- phox-forget-new-elim-command "edel elim %s.\n"
- phox-forget-new-intro-command "edel intro %s.\n"
- phox-forget-new-rewrite-command "edel rewrite %s.\n"
- phox-forget-close-def-command "edel closed %s.\n"
- phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
- phox-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
- phox-spaces-regexp "[ \n\t\r]*"
- phox-sy-definition-regexp (concat 
-   "\\(Cst\\|def\\)"
-   phox-comments-regexp
-   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
- phox-definition-regexp (concat
-   "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
-   phox-comments-regexp
-   phox-ident-regexp)
- phox-new-elim-regexp (concat
-   "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   phox-ident-regexp)
- phox-new-intro-regexp (concat
-   "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   phox-ident-regexp)
- phox-new-rewrite-regexp (concat
-   "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   phox-ident-regexp)
- phox-close-def-regexp (concat
-   "close_def"
-   phox-comments-regexp
-   "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
-)
-
-(defun phox-find-and-forget (span)
-  (let (str ans tmp (lsp -1))
-    (while span 
-      (setq str (span-property span 'cmd))
-
-      (cond
-
-       ((eq (span-property span 'type) 'comment))       
-
-       ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat (format phox-forget-id-command
-				  (span-property span 'name)) ans)))
-
-       ((proof-string-match phox-new-elim-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-elim-command 
-				  (match-string 3 str)) ans)))
-
-       ((proof-string-match phox-new-intro-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-intro-command 
-				  (match-string 3 str)) ans)))
-
-       ((proof-string-match phox-new-rewrite-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-rewrite-command 
-				  (match-string 3 str)) ans)))
-
-       ((proof-string-match phox-close-def-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-close-def-command 
-				  (match-string 4 str)) ans)))
-
-       ((proof-string-match phox-sy-definition-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-id-command 
-				  (concat "$" (match-string 7 str))) ans)))
-
-       ((proof-string-match phox-definition-regexp str)
-	(setq ans (concat (format phox-forget-id-command 
-				      (match-string 6 str)) ans))))
-
-
-      (setq lsp (span-start span))
-      (setq span (next-span span 'type)))
-
-      (or ans proof-no-command)))
-
-;;--------------------------------------------------------------------------;;
-;;
-;;    Deleting symbols
-;;
-;;--------------------------------------------------------------------------;;
-
-
-(defun phox-delete-symbol(symbol)
-  "Interactive function : 
-ask for a symbol and send a delete command to PhoX for it."
-  (interactive "ssymbol : ")
-  (proof-shell-invisible-command (concat "del " symbol ".\n")))
-
-(defun phox-delete-symbol-around-point()
-"Interactive function : 
-send a delete command to PhoX 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)))
-    (phox-delete-symbol (buffer-substring start end))))
-
-;;
-;; Doing commands
-;;
-
-(defun phox-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 (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (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 'phox-fun)
-
diff --git a/af2/phox-outline.el b/af2/phox-outline.el
deleted file mode 100644
index 766bddb3..00000000
--- a/af2/phox-outline.el
+++ /dev/null
@@ -1,57 +0,0 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                      PARAMÉTRAGE du MODE outline
-;;--------------------------------------------------------------------------;;
-
-
-(setq phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")
-(setq phox-outline-section-regexp "\\((\\*\\*+\\)")
-(setq phox-outline-save-regexp "\\((\\*#\\)")
-(setq 
- phox-outline-theo-regexp 
- "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)")
-(setq 
- phox-outline-theo2-regexp 
- "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)")
-
-(setq 
-  phox-outline-regexp 
-  (concat 
-   phox-outline-title-regexp "\\|" 
-   phox-outline-section-regexp "\\|" 
-   phox-outline-save-regexp "\\|" 
-   phox-outline-theo-regexp "\\|" 
-   phox-outline-theo2-regexp))
-
-(setq phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")
-
-;(if phox-outline
-;    (add-hook 'phox-mode-hook '(lambda()(outline-minor-mode 1)))
-;  )
-
-(defun phox-outline-level()
-  "Find the level of current outline heading in some PhoX libraries."
-  (let ((retour 0))
-    (save-excursion
-      (cond ((looking-at phox-outline-title-regexp) 1)
-	    ((looking-at phox-outline-section-regexp)
-	     (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6
-	    ((looking-at phox-outline-theo-regexp) 7)
-	    ((looking-at  (concat phox-outline-save-regexp "\\|"
-				 phox-outline-theo2-regexp )
-			 ) 8)
-	    )
-      )))
-
-(defun phox-setup-outline ()
-  "Set up local variable for outline mode"
-  (make-local-variable 'outline-heading-end-regexp)
-  (setq outline-heading-end-regexp phox-outline-heading-end-regexp)
-  (make-local-variable 'outline-regexp)
-  (setq outline-regexp phox-outline-regexp)
-  (make-local-variable 'outline-level)
-  (setq outline-level 'phox-outline-level)
-  (outline-minor-mode 1)
-)
-
-(provide 'phox-outline)
\ No newline at end of file
diff --git a/af2/phox-tags.el b/af2/phox-tags.el
deleted file mode 100644
index f2b5959a..00000000
--- a/af2/phox-tags.el
+++ /dev/null
@@ -1,77 +0,0 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                         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.
-
-(require 'etags) 
-
-(defun phox-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 phox-tags-reset-table()
-  "Set tags-table-list to nil."
-  (interactive)
-;  (make-local-variable 'tags-table-list)
-  (if proof-running-on-XEmacs
-      (progn
-	(setq tag-table-alist (remassoc buffer-file-name tag-table-alist)))
-    (setq tags-table-list nil))
-  )
-
-(defun phox-tags-add-doc-table()
-  "Add tags in text documentation."
-  (interactive)
-  (phox-tags-add-table (concat phox-doc-dir "/text/TAGS"))
-  )
-
-(defun phox-tags-add-lib-table()
-  "Add tags in libraries."
-  (interactive)
-  (phox-tags-add-table (concat phox-lib-dir "TAGS"))
-  )
- 
-(defun phox-tags-add-local-table()
-  "Add the tags table created with function phox-create-local-table."
-  (interactive)
-  (phox-tags-add-table (concat buffer-file-name "TAGS"))
-  )
-
-(defun phox-tags-create-local-table()
-  "create table on local buffer"
-  (interactive)
-  (shell-command (concat phox-etags 
-			 " -o " 
-			 (file-name-nondirectory (buffer-file-name))
-			 "TAGS "
-			 (file-name-nondirectory (buffer-file-name))))
-  )
-
-;; default
-
-(if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table))
-
-(provide 'phox-tags)
\ No newline at end of file
diff --git a/af2/phox.el b/af2/phox.el
deleted file mode 100644
index 49f4ab15..00000000
--- a/af2/phox.el
+++ /dev/null
@@ -1,229 +0,0 @@
-(require 'proof)			; load generic parts
-
-;; Adjust toolbar entries.  (Must be done
-;; before proof-toolbar is loaded).
-
-(if proof-running-on-XEmacs (setq phox-toolbar-entries
-      (remassoc 'context phox-toolbar-entries)))
-
-
-;; ======== User settings for PhoX ========
-;;
-;; Defining variables using customize is pretty easy.
-;; You should do it at least for your prover-specific user options.
-;;
-;; proof-site provides us with two customization groups
-;; automatically:  (based on the name of the assistant)
-;;
-;; 'phox        -  User options for PhoX Proof General
-;; 'phox-config -  Configuration of PhoX Proof General
-;;			   (constants, but may be nice to tweak)
-;;
-;; The first group appears in the menu
-;;   ProofGeneral -> Customize -> PhoX 
-;; The second group appears in the menu:
-;;   ProofGeneral -> Internals -> PhoX config
-;;
-
-(defcustom phox-prog-name "phox -pg"
-  "*Name of program to run PhoX."
-  :type 'file
-  :group 'phox)
-
-(defcustom phox-sym-lock t
-  "*Whether to use sym-lock or not."
-  :type 'boolean
-  :group 'phox)
-
-(defcustom phox-web-page
-  "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html"
-  "URL of web page for PhoX."
-  :type 'string
-  :group 'phox-config)
-
-(defcustom phox-doc-dir 
-  "/usr/local/doc/phox"
-  "The name of the root documentation directory for PhoX."
-  :type 'string
-  :group 'phox-config)
-
-(defcustom phox-lib-dir 
-  "/usr/local/lib/phox"
-  "The name of the root directory for PhoX libraries."
-  :type 'string
-  :group 'phox-config)
-
-(defcustom phox-tags-program 
-  (concat phox-doc-dir "/tools/phox_etags.sh")
-  "Program to run to generate TAGS table for proof assistant."
-  :type 'string
-  :group 'phox-config)
-
-(defcustom phox-tags-doc 
-  t
-  "*If non nil, tags table for PhoX text documentation is loaded."
-  :type 'boolean
-  :group 'phox-config)
-
-(defcustom phox-etags 
-  (concat phox-doc-dir "/tools/phox_etags.sh")
-  "Command to build tags table."
-  :type 'string
-  :group 'phox-config)
-
-(require 'phox-tags)
-(require 'phox-outline)
-(require 'phox-font)
-(require 'phox-fun)
-
-;; ----- PhoX specific menu
-
-(defpgdefault menu-entries
-  '(    
-    ["Delete symbol around cursor" phox-delete-symbol-around-point t]
-    ["Delete symbol" phox-delete-symbol t]
-    ["Compile theorem under cursor" phox-compile-theorem-around-point t]
-    "----"
-    ("Tags"
-     ["create a tags table for local buffer" phox-tags-create-local-table t]
-     ["------------------" nil nil]
-;    ["load table" phox-tags-load-table t]
-     ["add table"               phox-tags-add-table       t]
-     ["add local table"         phox-tags-add-local-table t]
-     ["add table for libraries" phox-tags-add-lib-table   t]
-     ["add table for text doc"  phox-tags-add-doc-table   t]
-     ["reset tags table list"   phox-tags-reset-table     t]
-     ["------------------" nil nil]
-     ["Find theorem, definition ..." find-tag t]
-     ["complete theorem, definition ..." complete-tag t]
-     )
-    ))
-
-;;
-;; ======== Configuration of generic modes ========
-;;
-
-(defun phox-config ()
-  "Configure Proof General scripting for PhoX."
-  (setq
-   proof-terminal-char		?\.	; ends every command
-   proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)"
-   proof-comment-start             "(*"
-   proof-comment-end               "*)"
-   proof-state-command             "goals."
-   proof-goal-command-regexp       "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
-   proof-save-command-regexp       "save"
-   proof-goal-with-hole-regexp     (concat 
-      "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)"
-      phox-comments-regexp
-      phox-ident-regexp)
-   proof-ignore-for-undo-count      "constraints\\|flags\\|goals\\|print\\|print_sort\\|eshow\\|search\\|priority\\|depend"
-   proof-goal-with-hole-result     5
-   proof-save-with-hole-regexp     (concat 
-      "save"
-      phox-comments-regexp
-      phox-ident-regexp)
-   proof-save-with-hole-result     4
-   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-find-and-forget-fn        'phox-find-and-forget
-   proof-find-theorems-command      "search \"%s\"."
-   proof-auto-multiple-files       nil
-   font-lock-keywords              phox-font-lock-keywords 
-   )
-)
-
-(defun phox-shell-config ()
-  "Configure Proof General shell for PhoX."
-  (setq
-   ;proof-shell-cd-cmd              "cd \"%s\""
-   proof-shell-prompt-pattern      "\\(>phox> \\)\\|\\(%phox% \\)"
-   proof-shell-annotated-prompt-regexp  "\\(>phox> \\)\\|\\(%phox% \\)"
-   proof-shell-interrupt-regexp    "Interrupt"
-   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 ========
-;;
-
-;; The name of the script mode is always <proofsym>-script,
-;; but the others can be whatever you like.
-;;
-;; The derived modes set the variables, then call the
-;; <mode>-config-done function to complete configuration.
-
-(define-derived-mode phox-mode proof-mode
-    "PhoX script" nil
-    (phox-config)
-    (phox-sym-lock-start)
-    (proof-config-done)
-    (phox-setup-outline)
-    (define-key phox-mode-map [(control j)] 
-      'phox-assert-next-command-interactive)
-    ;; with the previous binding,
-    ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed"
-
-    (define-key phox-mode-map [(control c) (meta d)] 
-      'phox-delete-symbol-around-point)  
-    ;; Configure syntax table for block comments
-    (modify-syntax-entry ?\* ". 23")
-    (modify-syntax-entry ?\( "()1")
-    (modify-syntax-entry ?\) ")(4"))
-
-(define-derived-mode phox-shell-mode proof-shell-mode
-   "PhoX shell" nil
-   (phox-shell-config)
-   (proof-shell-config-done))
-
-(define-derived-mode phox-response-mode proof-response-mode
-  "PhoX response" nil
-  (setq 
-   font-lock-keywords  phox-font-lock-keywords
-   proof-output-fontify-enable     t)
-  (phox-sym-lock-start)
-  (proof-response-config-done)
-  (font-lock-mode))
-
-(define-derived-mode phox-goals-mode proof-goals-mode
-  "PhoX goals" nil
-  (setq 
-   font-lock-keywords  phox-font-lock-keywords
-   proof-output-fontify-enable     t)
-  (phox-sym-lock-start)
-  (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
-;; would simply default to "proof-response-mode" and "pbp-mode".
-
-;; A more sophisticated instantiation might set font-lock-keywords to
-;; add highlighting, or some of the proof by pointing markup
-;; configuration for the goals buffer.
-
-;; The final piece of magic here is a hook which configures settings
-;; to get the proof shell running.  Proof General needs to know the
-;; name of the program to run, and the modes for the shell, response,
-;; and goals buffers.
-
-(add-hook 'proof-pre-shell-start-hook 'phox-pre-shell-start)
-
-(defun phox-pre-shell-start ()
-  (setq proof-prog-name		phox-prog-name)
-  (setq proof-mode-for-shell    'phox-shell-mode)
-  (setq proof-mode-for-response 'phox-response-mode)
-  (setq proof-mode-for-goals	'phox-goals-mode))
-
-(provide 'phox)
-
-
diff --git a/af2/sym-lock.el b/af2/sym-lock.el
deleted file mode 100644
index 085ef268..00000000
--- a/af2/sym-lock.el
+++ /dev/null
@@ -1,309 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; sym-lock.el - Extension of Font-Lock mode for symbol fontification.
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;        Copyright © 1997-1998 Albert Cohen, all rights reserved.
-;;         Copying is covered by the GNU General Public License.
-;;
-;;    This program is free software; you can redistribute it and/or modify
-;;    it under the terms of the GNU General Public License as published by
-;;    the Free Software Foundation; either version 2 of the License, or
-;;    (at your option) any later version.
-;;
-;;    This program is distributed in the hope that it will be useful,
-;;    but WITHOUT ANY WARRANTY; without even the implied warranty of
-;;    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-;;    GNU General Public License for more details.
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;                                 History
-;; 
-;; first prototype by wg <wg@cs.tu-berlin.de> 5-96
-;; tweaked by Steve Dunham <dunham@gdl.msu.edu> 5-96
-;; rewritten and enhanced by Albert Cohen <Albert.Cohen@prism.uvsq.fr> 3-97
-;; new symbol-face format and ergonomy improvement by Albert Cohen 2-98
-;; major step towards portability and customization by Albert Cohen 5-98
-;; removed bug with multiple appends in hook by Albert Cohen 3-99
-;; removed sym-lock-face&atom which where not working by C Raffalli 4-2000 
-
-;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
-
-(require 'font-lock)
-(require 'atomic-extents)
-
-(defvar sym-lock-sym-count 0
-  "Counter for internal symbols.")
-
-(defvar sym-lock-ext-start nil "Temporary for atomicization.")
-(make-variable-buffer-local 'sym-lock-ext-start)
-(defvar sym-lock-ext-end nil "Temporary for atomicization.")
-(make-variable-buffer-local 'sym-lock-ext-end)
-
-(defvar sym-lock-font-size nil
-  "Default size for Sym-Lock symbol font.")
-(make-variable-buffer-local 'sym-lock-font-size)
-(put 'sym-lock-font-size 'permanent-local t)
-
-(defvar sym-lock-keywords nil
-  "Similar to `font-lock-keywords'.")
-(make-variable-buffer-local 'sym-lock-keywords)(put 'sym-lock-keywords 'permanent-local t)
-
-(defvar sym-lock-enabled nil
-  "Sym-Lock switch.")
-(make-variable-buffer-local 'sym-lock-enabled)
-(put 'sym-lock-enabled 'permanent-local t)
-
-(defvar sym-lock-color (face-foreground 'default)
-  "*Sym-Lock default color in `font-lock-use-colors' mode.")
-(make-variable-buffer-local 'sym-lock-color)
-(put 'sym-lock-color 'permanent-local t)
-
-(defvar sym-lock-mouse-face 'default
-  "*Face for symbols when under mouse.")
-(make-variable-buffer-local 'sym-lock-mouse-face)
-(put 'sym-lock-mouse-face 'permanent-local t)
-
-(defvar sym-lock-mouse-face-enabled t
-  "Mouse face switch.")
-(make-variable-buffer-local 'sym-lock-mouse-face-enabled)
-(put 'sym-lock-mouse-face-enabled 'permanent-local t)
-
-(defun sym-lock-gen-symbol (&optional prefix)
-  "Generate a new internal symbol."
-  ;; where is the standard function to do this ?
-  (setq sym-lock-sym-count (+ sym-lock-sym-count 1))
-  (intern (concat "sym-lock-gen-" (or prefix "") 
-		  (int-to-string sym-lock-sym-count))))
-
-(defun sym-lock-make-symbols-atomic (&optional begin end)
-  "Function to make symbol faces atomic."
-  (if sym-lock-enabled
-      (map-extents 
-       (lambda (extent maparg)
-	 (let ((face (extent-face extent)) (ext))
-	   (if (and face (setq ext (face-property face 'sym-lock-remap)))
-	       (progn
-		 (if (numberp ext)
-		     (set-extent-endpoints
-		      extent (- (extent-start-position extent) ext)
-		      (extent-end-position extent)))
-		 (if ext
-		     (progn
-		       (if sym-lock-mouse-face-enabled
-			   (set-extent-property extent 'mouse-face
-						sym-lock-mouse-face))
-		       (set-extent-property extent 'atomic t)
-		       (set-extent-property extent 'start-open t))))))
-	 nil)
-       (current-buffer)
-       (if begin (save-excursion (goto-char begin) (beginning-of-line) (point))
-	 (point-min))
-       (if end (save-excursion (goto-char end) (end-of-line) (point))
-	 (point-max))
-       nil nil)))
-
-(defun sym-lock-compute-font-size ()
-  "Computes the size of the \"better\" symbol font."
-  (let ((num (if (fboundp 'face-height)
-		 (face-height 'default)
-	       (let ((str (face-font 'default)))
-		 (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)
-      (if 
-	  (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*"
-		    (car lf))
-	  (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
-  (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)
-
-(make-face 'sym-lock-adobe-symbol-face)
-(set-face-font 'sym-lock-adobe-symbol-face sym-lock-font-name)
-
-(defun sym-lock-set-foreground ()
-  "Set foreground color of Sym-Lock faces."
-  (if (and (boundp 'sym-lock-defaults) sym-lock-defaults)
-      (let ((l (car sym-lock-defaults))
-	    (color (if (and (boundp 'font-lock-use-fonts) font-lock-use-fonts)
-		       (face-foreground 'default) sym-lock-color)))
-	(if (and (consp l) (eq (car l) 'quote)) (setq l (eval l)))
-	(if (symbolp l) (setq l (eval l)))
-	(dolist (c l)
-	  (setq c (nth 2 c))
-	  (if (consp c) (setq c (eval c)))
-	  (if (string-match "-adobe-symbol-" (font-name (face-font c)))
-	      (set-face-foreground c color))))))
-
-(defun sym-lock-remap-face (pat pos obj atomic)
-  "Make a temporary face which remaps the POS char of PAT to the
-given OBJ under `sym-lock-adobe-symbol-face' and all other characters to
-the empty string. OBJ may either be a string or a character."
-  (let* ((name (sym-lock-gen-symbol "face"))
-	 (table (make-display-table))
-	 (tface (make-face name "sym-lock-remap-face" t)))
-    (fillarray table "")
-    (aset table (string-to-char (substring pat (1- pos) pos))
-	  (if (stringp obj) obj (make-string 1 obj)))
-    (set-face-foreground tface (if (and (boundp 'font-lock-use-fonts)
-					font-lock-use-fonts)
-				   (face-foreground 'default) sym-lock-color))
-    (set-face-property tface 'display-table table)
-    (set-face-property tface 'font (face-font 'sym-lock-adobe-symbol-face))
-    (set-face-property tface 'sym-lock-remap atomic) ; mark it
-    tface  ; return face value and not face name
-	   ; the temporary face would be otherwise GCed
-    ))
-
-(defvar sym-lock-clear-face
-  (let* ((name (sym-lock-gen-symbol "face"))
-	 (table (make-display-table))
-	 (tface (make-face name "sym-lock-remap-face" t)))
-    (fillarray table "")
-    (set-face-property tface 'display-table table)
-    (set-face-property tface 'sym-lock-remap 1) ; mark it
-    tface 
-    ;; return face value and not face name
-    ;; the temporary face would be otherwise GCed
-    ))
-
-(defun sym-lock (fl)
-  "Create font-lock table entries from a list of (PAT NUM POS OBJ) where
-PAT (at NUM) is substituted by OBJ under `sym-lock-adobe-symbol-face'. The
-face's extent will become atomic."
-  (message "Computing Sym-Lock faces...")
-  (setq sym-lock-keywords (sym-lock-rec fl))
-  (setq sym-lock-enabled t)
-  (message "Computing Sym-Lock faces... done."))
-
-(defun sym-lock-rec (fl)
-  (let ((f (car fl)))
-    (if f 	      
-	(cons (apply 'sym-lock-atom-face f)
-	      (sym-lock-rec (cdr fl))))))
-
-(defun sym-lock-atom-face (pat num pos obj &optional override)
-  "Define an entry for the font-lock table which substitutes PAT (at NUM) by
-OBJ under `sym-lock-adobe-symbol-face'. The face extent will become atomic."
-  (list pat num (sym-lock-remap-face pat pos obj t) override))
-
-(defun sym-lock-pre-idle-hook-first ()
-  (condition-case nil
-      (if (and sym-lock-enabled font-lock-old-extent)
-	  (setq sym-lock-ext-start (extent-start-position font-lock-old-extent)
-		sym-lock-ext-end (extent-end-position font-lock-old-extent))
-	(setq sym-lock-ext-start nil))
-    (error (warn "Error caught in `sym-lock-pre-idle-hook-first'"))))
-
-(defun sym-lock-pre-idle-hook-last ()
-  (condition-case nil
-      (if (and sym-lock-enabled sym-lock-ext-start)
-	  (sym-lock-make-symbols-atomic sym-lock-ext-start sym-lock-ext-end))
-    (error (warn "Error caught in `sym-lock-pre-idle-hook-last'"))))
-
-(add-hook 'font-lock-after-fontify-buffer-hook
-	  'sym-lock-make-symbols-atomic)
-
-(defun sym-lock-enable ()
-  "Enable Sym-Lock on this buffer."
-  (interactive)
-  (if (not sym-lock-keywords)
-      (error "No Sym-Lock keywords defined!")
-    (setq sym-lock-enabled t)
-    (if font-lock-mode
-	(progn
-	  (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug!
-	  (font-lock-set-defaults t)
-	  (font-lock-fontify-buffer)))
-    (message "Sym-Lock enabled.")))
-
-(defun sym-lock-disable ()
-  "Disable Sym-Lock on this buffer."
-  (interactive)
-  (if (not sym-lock-keywords)
-      (error "No Sym-Lock keywords defined!")
-    (setq sym-lock-enabled nil)
-    (if font-lock-mode
-	(progn
-	  (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug!
-	  (font-lock-set-defaults t)
-	  (font-lock-fontify-buffer)))
-    (message "Sym-Lock disabled.")))
-
-(defun sym-lock-mouse-face-enable ()
-  "Enable special face for symbols under mouse."
-  (interactive)
-  (setq sym-lock-mouse-face-enabled t)
-  (if sym-lock-enabled
-      (font-lock-fontify-buffer)))
-
-(defun sym-lock-mouse-face-disable ()
-  "Disable special face for symbols under mouse."
-  (interactive)
-  (setq sym-lock-mouse-face-enabled nil)
-  (if sym-lock-enabled
-      (font-lock-fontify-buffer)))
-
-(defun sym-lock-font-lock-hook ()
-  "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
-	(sym-lock-patch-keywords)
-	(sym-lock-set-foreground))))
-
-(defun font-lock-set-defaults (&optional explicit-defaults)
-  (when
-      (and
-       (featurep 'font-lock)
-       (if font-lock-auto-fontify
-           (not (memq major-mode font-lock-mode-disable-list))
-         (memq major-mode font-lock-mode-enable-list))
-       (font-lock-set-defaults-1 explicit-defaults)
-       (sym-lock-patch-keywords))
-    (turn-on-font-lock)))
-
-(defun sym-lock-patch-keywords ()
-  (if (and font-lock-keywords sym-lock-enabled
-	   (boundp 'sym-lock-keywords)
-	   (listp (car font-lock-keywords))
-	   (listp (cdar font-lock-keywords))
-	   (listp (cddar font-lock-keywords))
-	   (or (listp (caddar font-lock-keywords))
-	       (not (string-match
-		     "sym-lock"
-		     (symbol-name
-		      (face-name (cadr (cdar
-					font-lock-keywords))))))))
-      (setq font-lock-keywords (append sym-lock-keywords
-				       font-lock-keywords))) t)
-
-(add-hook 'font-lock-mode-hook 'sym-lock-font-lock-hook)
-
-(provide 'sym-lock)