New files.

1 files changed, 96 insertions, 0 deletions

diff --git a/lib/pg-dev.el b/lib/pg-dev.el
new file mode 100644
index 00000000..90e3d2bd
--- /dev/null
+++ b/lib/pg-dev.el
@@ -0,0 +1,96 @@
+;;; pg-dev.el --- Developer settings for Proof General
+;;
+;; Copyright (C) 2008 LFCS Edinburgh.
+;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;;
+;;; Commentary:
+;; 
+;; Some configuration of Emacs Lisp mode for developing PG, not needed
+;; for ordinary users.
+;;
+
+;; Use checkdoc, eldoc, Flyspell:
+
+;;; Code:
+(add-hook 'emacs-lisp-mode-hook
+	  '(lambda () (checkdoc-minor-mode 1)))
+
+(add-hook 'emacs-lisp-mode-hook 'turn-on-eldoc-mode)
+
+(add-hook 'emacs-lisp-mode-hook 'flyspell-prog-mode)
+
+
+;; Configure indentation for our macros
+
+(put 'proof-if-setting-configured 'lisp-indent-function 1)
+(put 'proof-eval-when-ready-for-assistant 'lisp-indent-function 1)
+(put 'proof-define-assistant-command 'lisp-indent-function 'defun)
+(put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun)
+(put 'defpgcustom 'lisp-indent-function 'defun)
+(put 'proof-map-buffers 'lisp-indent-function 'defun)
+(put 'proof-with-current-buffer-if-exists 'lisp-indent-function 'defun)
+
+FIXME: see font-lock.el
+(defconst pg-dev-lisp-font-lock-keywords
+  (list
+   (concat "(\\(def\\(" ;; also proof-def
+	   ;; Function like things
+	   "^(\\(proof-def.*\\|defpg.*\\|defpa.*\\|.*asscustom\\)"
+	   ;; Variable like things
+    "\\([^ \t\n\(\)]*\\)"
+    ;; Any whitespace and declared object.
+    "[ \t'\(]*"
+    "\\([^ \t\n\)]+\\)?")
+   '(1 font-lock-keyword-face)
+   '(8 (cond ((match-beginning 3) 'font-lock-variable-name-face)
+	     ;; ((match-beginning 6) 'font-lock-type-face)
+	     (t 'font-lock-function-name-face))
+       nil t)))
+
+(add-hook 'emacs-lisp-mode-hook
+	  '(lambda ()
+	     (font-lock-add-keywords 'emacs-lisp-mode
+				     pg-dev-lisp-font-lock-keywords)))
+
+
+;;;
+;;; Autoloads (as used by "make autoloads")
+;;;
+
+(setq autoload-package-name "proof")
+(setq generated-autoload-file "proof-autoloads.el")
+
+;;;
+;;; Unload utility (not wholly successful)
+;;;
+
+(defun unload-pg ()
+  "Attempt to unload Proof General (for development use only)."
+  (interactive)
+  (mapcar
+   (lambda (feat) (condition-case nil
+		    (unload-feature feat 'force)
+		    (error nil)))
+   '(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
+     proof-shell pg-metadata proof-menu pg-pbrpm pg-pgip proof-script
+     proof-autoloads pg-response pg-goals pg-pgip-old proof-toolbar
+     proof-easy-config proof-config proof-mmm proof pg-xhtml
+     proof-utils proof-syntax proof-system pg-user proof-x-symbol
+     pg-thymodes pg-autotest
+     ;; 
+     isar-syntax isar-find-theorems x-symbol-isar
+     isar-autotest interface-setup isabelle-system isar isar-mmm
+     isar-keywords
+     ;;
+     coq-abbrev coq-db x-symbol-coq coq-local-vars coq coq-syntax
+     coq-indent coq-autotest)))
+
+     
+
+
+
+(provide 'pg-dev)
+
+;;; pg-dev.el ends here