af2 is now called PhoX

8 files changed, 988 insertions, 0 deletions

diff --git a/phox/README b/phox/README
new file mode 100644
index 00000000..9c955b84
--- /dev/null
+++ b/phox/README
@@ -0,0 +1,19 @@
+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/phox/example.af2 b/phox/example.af2
new file mode 100644
index 00000000..36ece411
--- /dev/null
+++ b/phox/example.af2
@@ -0,0 +1,9 @@
+(*
+    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/phox/phox-font.el b/phox/phox-font.el
new file mode 100644
index 00000000..f04844fa
--- /dev/null
+++ b/phox/phox-font.el
@@ -0,0 +1,138 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;;                       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/phox/phox-fun.el b/phox/phox-fun.el
new file mode 100644
index 00000000..58771057
--- /dev/null
+++ b/phox/phox-fun.el
@@ -0,0 +1,150 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;; 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/phox/phox-outline.el b/phox/phox-outline.el
new file mode 100644
index 00000000..766bddb3
--- /dev/null
+++ b/phox/phox-outline.el
@@ -0,0 +1,57 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;;                      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/phox/phox-tags.el b/phox/phox-tags.el
new file mode 100644
index 00000000..f2b5959a
--- /dev/null
+++ b/phox/phox-tags.el
@@ -0,0 +1,77 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;;                         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/phox/phox.el b/phox/phox.el
new file mode 100644
index 00000000..49f4ab15
--- /dev/null
+++ b/phox/phox.el
@@ -0,0 +1,229 @@
+(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/phox/sym-lock.el b/phox/sym-lock.el
new file mode 100644
index 00000000..085ef268
--- /dev/null
+++ b/phox/sym-lock.el
@@ -0,0 +1,309 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 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)