diff options
| -rw-r--r-- | demoisa/demoisa-easy.el | 63 | ||||
| -rw-r--r-- | generic/proof-easy-config.el | 57 |
2 files changed, 35 insertions, 85 deletions
diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el index 7aee3db5..71262d03 100644 --- a/demoisa/demoisa-easy.el +++ b/demoisa/demoisa-easy.el @@ -1,4 +1,4 @@ -;; demoisa-easy.el Example Proof General instance for Isabelle +;; proof-easy.el Example Proof General instance for Isabelle ;; ;; Copyright (C) 1999 LFCS Edinburgh. ;; @@ -8,51 +8,46 @@ ;; ;; This is an alternative version of demoisa.el which uses the ;; proof-easy-config mechanism to avoid declaring derived modes, etc. -;; -;; NB: proof-easy-config is experimental, and only works with XEmacs. +;; NB: proof-easy-config is experimental. ;; ;; See demoisa.el for documentation. ;; ;; To test this file you must rename it demoisa.el. -;; -;; It relies on this line in proof-assistant-table: -;; demoisa "Isabelle Demo" "\\.ML$" -;; (require 'proof-easy-config) ; easy configure mechanism (proof-easy-config 'demoisa "Isabelle Demo" - demoisa-prog-name "isabelle" - demoisa-terminal-char ?\; - demoisa-comment-start "(*" - demoisa-comment-end "*)" - demoisa-goal-command-regexp "^Goal" - demoisa-save-command-regexp "^qed" - demoisa-goal-with-hole-regexp "^Goal \\(\\(\"%s\"\\)\\)" - demoisa-save-with-hole-regexp "^qed \\(\\(\"%s\"\\)\\)" - demoisa-non-undoables-regexp "undo\\|back" - demoisa-undo-n-times-cmd "pg_repeat undo %s;" - demoisa-showproof-command "pr()" - demoisa-goal-command "Goal \"%s\";" - demoisa-save-command "qed \"%s\";" - demoisa-kill-goal-command "Goal \"PROP no_goal_set\";" - demoisa-auto-multiple-files t - demoisa-shell-cd-cmd "cd \"%s\"" - demoisa-shell-prompt-pattern "[ML-=#>]+>? " - demoisa-shell-interrupt-regexp "Interrupt" - demoisa-shell-start-goals-regexp "Level [0-9]" - demoisa-shell-end-goals-regexp "val it" - demoisa-shell-quit-cmd "quit();" - demoisa-assistant-home-page + proof-prog-name "isabelle" + proof-terminal-char ?\; + proof-comment-start "(*" + proof-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "^Goal \\(\\(\"%s\"\\)\\)" + proof-save-with-hole-regexp "^qed \\(\\(\"%s\"\\)\\)" + proof-non-undoables-regexp "undo\\|back" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-showproof-command "pr()" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-quit-cmd "quit();" + proof-assistant-home-page "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html" - demoisa-shell-annotated-prompt-regexp + proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " - demoisa-shell-error-regexp + proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " - demoisa-shell-init-cmd + proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" - demoisa-shell-demoisa-completed-regexp + proof-shell-proof-completed-regexp "\\(\\(.\\|\n\\)*No subgoals!\n\\)" - demoisa-shell-eager-annotation-start + proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading") diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index 696e6a34..81ec4f26 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -6,40 +6,12 @@ ;; ;; $Id$ ;; -;; Work in progress. -;; -;; XEmacs only at the moment (uses defvaralias) -;; -;; Future version might copy settings instead. Consider how best to +;; Future version might copy settings instead; consider how best to ;; interface with customization mechanism so a new prover can be ;; configured by editing inside custom buffers. ;; - (require 'proof) -(unless (fboundp 'defvaralias) - (error "proof-easy-config only works for XEmacs, sorry!")) - -(autoload 'custom-group-members "cus-edit") - - -(defun proof-easy-config-make-var-aliases (sym group) - "Make variable aliases for custom GROUP, with new prefix SYM." - (let ((vars (custom-group-members group nil)) - (prefix (length - (or (get 'custom-prefix group) ; fails sometimes, why? - "proof-"))) ; common prefix - (newpref (concat (symbol-name sym) "-"))) - (dolist (cusmem vars) - (cond ((member 'custom-group cusmem) - ;; recurse on subgroups - (proof-easy-config-make-var-aliases sym (car cusmem))) - ((member 'custom-variable cusmem) - (let* ((thisone (car cusmem)) - (base (substring (symbol-name thisone) prefix)) - (alias (intern (concat newpref base)))) - (defvaralias alias thisone))))))) - (defvar proof-easy-config-derived-modes-table '(("" "script" proof-mode (proof-config-done)) ("shell" "shell" proof-shell-mode (proof-shell-config-done)) @@ -47,9 +19,6 @@ ("goals" "goals" pbp-mode (proof-goals-config-done))) "A list of (PREFIXSYM SUFFIXNAME PARENT MODEBODY) for derived modes.") -;; FIXME: Non-uniformity in current code -(defvaralias 'proof-mode-for-goals 'proof-mode-for-pbp) - (defun proof-easy-config-define-derived-modes () (dolist (modedef proof-easy-config-derived-modes-table) (let* ((prefixsym (nth 0 modedef)) @@ -58,30 +27,16 @@ (body (nthcdr 3 modedef)) (modert (concat (symbol-name proof-assistant-symbol) "-" prefixsym)) - ; config function for mode -- don't need it with global settings. - ; (modecfgfn (intern (concat modert "-config"))) (hyphen (if (string-equal prefixsym "") "" "-")) (mode (intern (concat modert hyphen "mode"))) (modename (concat proof-assistant " " suffixnm)) (varname (intern (concat "proof-mode-for-" suffixnm)))) - (eval `(define-derived-mode ,mode ,parent ,modename nil ,@body)) - - ;; Set proof-mode-for-script, etc. NB: at top-level rather - ;; than in function body. Then we don't need to set - ;; proof-pre-shell-start-hook. + ;; Set proof-mode-for-script and friends + ;; NB: top-level, so we don't need proof-pre-shell-start-hook. (set varname mode)))) -(defun proof-easy-config-define-customs () - "Define a -prog-name customization setting." - (let* ((pn-def (symbol-name proof-assistant-symbol)) - (pn (intern (concat pn-def "-prog-name")))) - `(defcustom ,pn ,pn-def - ,(concat "*Name of program to run " proof-assistant) - :type 'string - :group ,proof-assistant-symbol))) - (defun proof-easy-config-check-setup (sym name) "A number of simple checks." (cond @@ -102,11 +57,11 @@ "Configure Proof General for proof-assistant using BODY as a setq body." `(progn (proof-easy-config-check-setup ,sym ,name) - (proof-easy-config-make-var-aliases ,sym 'prover-config) - (proof-easy-config-define-customs) (setq ,@body) - (proof-easy-config-define-derived-modes))) + (proof-easy-config-define-derived-modes) + ;; FIXME: Non-uniformity in current code + (setq proof-mode-for-goals proof-mode-for-pbp))) ;; (provide 'proof-easy-config) |