diff options
| -rw-r--r-- | lego.el | 654 | ||||
| -rw-r--r-- | pbp.el | 300 | ||||
| -rw-r--r-- | proof.el | 546 |
3 files changed, 1500 insertions, 0 deletions
diff --git a/lego.el b/lego.el new file mode 100644 index 00000000..ad0e6246 --- /dev/null +++ b/lego.el @@ -0,0 +1,654 @@ +;; lego.el Major mode for LEGO proof assistants +;; Copyright (C) 1994, 1995, 1996 LFCS Edinburgh. +;; This version by Dilip Sequeira, by rearranging Thomas Schreiber's +;; code. + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; Time-stamp: <01 Mar 97 tms /home/tms/elisp/lego.el> +;; Thanks to David Aspinall, Robert Boyer, Rod Burstall, +;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens + +(require 'pbp) +(require 'easymenu) +(require 'font-lock) +(require 'outline) + +; Configuration + +(defconst lego-mode-version-string + "LEGO-MODE. ALPHA Version 1.11 (June 1996) LEGO Team <lego@dcs.ed.ac.uk>") + +(defvar lego-tags "/usr/local/share/lego/lib-alpha/lib_all/TAGS" + "the default TAGS table for the LEGO library") + +(defvar lego-pretty-p t + "In the latest version of LEGO, pretty printing using Oppen's + algorithm can be switched on, but is disabled. The Emacs interface + is primarily concerned to make life easier. There it will enable + pretty printing") + +(defconst lego-pretty-on "Configure PrettyOn;" + "Command to enable pretty printing of the LEGO process.") + +(defconst lego-annotate-on "Configure AnnotateOn;" + "Command to enable pretty printing of the LEGO process.") + +(defconst lego-pretty-set-width "Configure PrettyWidth %s;" + "Command to adjust the linewidth for pretty printing of the LEGO + process.") + +(defvar lego-test-all-name "test_all" + "The name of the LEGO module which inherits all other modules of the + library.") + +;; Could be set to "Load". To cite Mark, "Although this may sound +;; strange at first side, the Make command is much, much slower for my +;; files then the load command. That is because .o files do not save +;; Equiv's. So a Make of a .o file needs to find the proper +;; conversions itself, and hence will be much slower in some +;; cases. Especially when doing larger examples." + +(defvar lego-make-command "Make") + +(defvar lego-path-name "LEGOPATH" + "The name of the environmental variable to search for modules. This + is used by \\{legogrep} to find the files corresponding to a + search.") + +(defvar lego-path-separator ":" + "A character indicating how the items in the \\{lego-path-name} are + separated.") + +(defvar lego-save-query t + "*If non-nil, ask user for permission to save the current buffer before + processing a module.") + + +;; ----- web documentation + +(defvar lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/") + +(defvar lego-www-refcard (concat (w3-remove-file-name lego-www-home-page) + "refcard.dvi.gz")) + +;; `lego-www-refcard' ought to be set to +;; "ftp://ftp.dcs.ed.ac.uk/pub/lego/refcard.dvi.gz", but +;; a) w3 fails to decode the image before invoking xdvi +;; b) ange-ftp and efs cannot handle Solaris ftp servers + + +(defvar lego-library-www-page + (concat (w3-remove-file-name lego-www-home-page) + "html/library/newlib.html")) + +(defvar lego-www-customisation-page + (concat (w3-remove-file-name lego-www-home-page) + "html/emacs-customisation.html")) + +;; ----- legostat and legogrep, courtesy of Mark Ruys + +(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) + "Last legogrep command used in \\{legogrep}; default for next legogrep.") + +(defvar legostat-command "legostat -t") + +(defvar legogrep-regexp-alist + '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) + "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") + +;; ----- lego-shell configuration options + +(defvar lego-shell-process-name "lego" + "*The name of the lego-process") + +(defvar lego-shell-prog-name "legoML" + "*Name of program to run as lego.") + +(defvar lego-shell-working-dir "" + "The working directory of the lego shell") + +(defvar lego-shell-prompt-pattern "^\\(Lego>[ \t]*\\)+" + "*The prompt pattern for the inferion shell running lego.") + +(defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state" + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" + "*Regular expression indicating that the proof has been completed.") + +;; ----- outline + +(defvar lego-goal-regexp "\\?\\([0-9]+\\)") + +(defvar lego-outline-regexp + (concat "[[*]\\|" + (ids-to-regexp + '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" + "Unfreeze")))) + +(defvar lego-outline-heading-end-regexp ";\\|\\*)") + +(defvar lego-shell-outline-regexp lego-goal-regexp) +(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp) + +;; ----- keywords for font-lock. If you want to hack deeper, you'd better +;; ----- be fluent in regexps - it's in the YUK section. + +(defvar lego-keywords-goal '("$?Goal")) + +(defvar lego-keywords-save + '("$?Save")) + +(defvar lego-keywords + (append lego-keywords-goal lego-keywords-save + '("allE" "allI" "andE" "andI" "Assumption" "Claim" + "Constructors" "Cut" "Discharge" "DischargeKeep" + "Double" "echo" "ElimOver" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "Fields" "Freeze" "From" "Hnf" "Immed" + "impE" "impI" "Import" "Induction" "Inductive" "Inversion" "Init" + "intros" "Intros" "Module" "Next" "NoReductions" "Normal" "notE" + "notI" "orE" "orIL" "orIR" "Parameters" "Qnify" "Qrepl" "Record" + "Refine" "Relation" "Theorems" "Unfreeze"))) + +(defvar lego-shell-keywords + '("Cd" "Ctxt" "Decls" "Forget" "ForgetMark" "Help" "KillRef" "Load" + "Make" "Prf" "Pwd" "Help" "KillRef" "Load" "Make" "Prf" "Pwd" + "Reload" "Undo")) + +(defvar lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) + + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-derived-mode lego-shell-mode comint-mode + "lego-shell" "Inferior shell mode for lego shell" + (lego-shell-mode-config)) + +(define-derived-mode lego-mode proof-mode + "lego" "Lego Mode" + (lego-mode-config)) + +(define-derived-mode lego-pbp-mode pbp-mode + "pbp" "Proof-by-pointing support for LEGO" + (lego-pbp-mode-config)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Popup and Pulldown Menu ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar lego-shared-menu + (append '( + ["Display context" lego-ctxt + :active (proof-shell-buffer)] + ["Display proof state" lego-prf + :active (proof-shell-buffer)] + ["Restart the proof" lego-restart-goal + :active (proof-shell-buffer)] + ["Kill the current refinement proof" + lego-killref :active (proof-shell-buffer)] + ["Undo last proof step" lego-undo-1 + :active (proof-shell-buffer)] + ["Exit LEGO" proof-shell-exit + :active (proof-shell-buffer)] + "----" + ["Find definition/declaration" find-tag-other-window t] + ("Help" + ["The LEGO Reference Card" (w3-fetch lego-www-refcard) t] + ["The LEGO library (WWW)" + (w3-fetch lego-library-www-page) t] + ["The LEGO Proof-assistant (WWW)" + (w3-fetch lego-www-home-page) t] + ["Help on Emacs LEGO-mode" describe-mode t] + ["Customisation" (w3-fetch lego-www-customisation-page) + t] + )))) + +(defvar lego-process-menu + '("Process LEGO code" + ["Process buffer" lego-make-buffer t] + ["Process buffer until point" lego-make-buffer-until-point + t] + ["Process command" proof-send-command t] + ["Process line" proof-send-line t] + ["Process region" proof-send-region t]) + "*Interaction between the proof script and the LEGO process.") + +(defvar lego-menu + (append '("LEGO Commands" + ["Start LEGO" lego-shell + :active (not (comint-check-proc (and proof-shell-process-name + (proof-shell-buffer))))] + ["Toggle active ;" proof-active-terminator-minor-mode + :active t + :style toggle + :selected proof-active-terminator-minor-mode] + "----") + (list lego-process-menu) + '("----") + (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) + "--:doubleLine" "----")) + lego-shared-menu + ) + "*The menu for LEGO.") + +(defvar lego-shell-menu lego-shared-menu + "The menu for the LEGO shell") + +(easy-menu-define lego-shell-menu + lego-shell-mode-map + "Menu used in the lego shell." + (cons "LEGO" (cdr lego-shell-menu))) + +(easy-menu-define lego-mode-menu + lego-mode-map + "Menu used lego mode." + (cons "LEGO" (cdr lego-menu))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; * * * * * * ;; +;; * * * * * * ;; +;; * * * **** ;; +;; * * * * * ;; +;; * * * * * ;; +;; * **** * * ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" + "A regular expression indicating that the LEGO process has + identified an error.") + +(defvar lego-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing LEGO identifiers.") + +(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") + "*For font-lock, we treat \",\" separated identifiers as one identifier + and refontify commata using \\{lego-fixup-change}.") + +(defun lego-decl-defn-regexp (char) + (concat "\\[\\s *\\(" lego-ids + "\\)\\s *\\(\\[[^]]+\\]\\s *\\)*" char)) +; Examples +; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ +; [ sort = +; [ sort [n:nat] = +; [ sort [abbrev=...][n:nat] = + +(defvar lego-font-lock-terms + (list + + ; lambda binders + (list (lego-decl-defn-regexp "[:|]") 1 + 'font-lock-declaration-name-face) + + ; let binders + (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) + + ; Pi and Sigma binders + (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 + 'font-lock-declaration-name-face t) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\((" + lego-id ")\\)?") 'font-lock-type-face)) + "*Font-lock table for LEGO terms.") + +(defvar lego-font-lock-keywords-1 + (append + lego-font-lock-terms + (list + (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face) + (cons (ids-to-regexp lego-tacticals) 'font-lock-tacticals-name-face) + + (list (concat "\\(" + (ids-to-regexp lego-keywords-goal) + "\\)\\s *\\(" lego-id "\\)\\s *:") + 2 'font-lock-function-name-face) + + (list (concat "\\(" + (ids-to-regexp lego-keywords-save) + "\\)\\s *\\(" lego-id "\\)") + 2 'font-lock-function-name-face)))) + + +(defvar lego-shell-font-lock-keywords-1 + (append lego-font-lock-keywords-1 + (list + (cons (ids-to-regexp lego-shell-keywords) + 'font-lock-keyword-face) + + (list (concat "\\<defn\\> \\(" lego-id "\\) =") 1 + 'font-lock-function-name-face) + + (list (concat "^\\(value of\\|type of\\) \\(" lego-id "\\) =") 2 + 'font-lock-function-name-face) + + (list (concat "^ \\(" lego-id "\\) = ... :") 1 + 'font-lock-function-name-face) + + (list (concat "^ \\(" lego-id "\\) [:|]") 1 + 'font-lock-declaration-name-face) + + ; e.g., decl S1 S2 : prog sort + (list (concat "\\<decl\\> \\(" lego-id + "\\( " lego-id "\\)*\\) [:|] ") 1 + 'font-lock-declaration-name-face) + + (list (concat "^value = \\(" lego-id "\\)") 1 + 'font-lock-declaration-name-face)))) +;; +;; A big hack to unfontify commas in declarations and definitions. All +;; that can be said for it is that the previous way of doing this was +;; even more bogus. +;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun lego-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point))))))) + +(defun lego-zap-commas-buffer () + (lego-zap-commas-region (point-min) (point-max) 0)) + +(defun lego-fixup-change () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'lego-zap-commas-region after-change-functions) + '(lego-zap-commas-region)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's lego specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Martin Steffen <mnsteffe@informatik.uni-erlangen.de> has pointed +;; out that calling lego-get-path has to deal with a user who hasn't +;; set the environmental variable LEGOPATH. It is probably best if +;; lego is installed as a shell script which sets a sensible default +;; for LEGOPATH if the user hasn't done so before. See the +;; documentation of the library for further details. + +(defun lego-get-path () + (let ((path-name (getenv lego-path-name))) + (cond ((not path-name) + (message "Warning: LEGOPATH has not been set!") + (setq path-name "."))) + (string-to-list path-name lego-path-separator))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to lego ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-restart-goal () + "Restart the current proof." + (interactive) + (proof-command "Undo 9999")) ;hopefully 9999 is large + ;enough! +(defun lego-killref () + "Kill the current refinement proof." + (interactive) + (proof-command "KillRef")) + +(defun lego-help () + "Print help message giving syntax." + (interactive) + (proof-command "Help")) + +(defun lego-undo-1 () + "Undo the last step in a proof." + (interactive) + (proof-command "Undo 1")) + +(defun lego-prf () + "List proof state." + (interactive) + (proof-command "Prf")) + +(defun lego-ctxt () + "List context." + (interactive) + (proof-command "Ctxt")) + +(defun lego-intros () + "intros." + (interactive) + (insert "intros ")) + +(defun lego-Intros () + "List proof state." + (interactive) + (insert "Intros ")) + +(defun lego-Refine () + "List proof state." + (interactive) + (insert "Refine ")) + +(defun lego-shell () + "Start a lego shell" + (interactive) + (proof-start-shell)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lego shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar lego-shell-current-line-width nil + "Current line width of the LEGO process's pretty printing module. + Its value will be updated whenever the corresponding screen gets + selected.") + +;; The line width needs to be adjusted if the LEGO process is +;; running and is out of sync with the screen width + +(defun lego-adjust-line-width () + "Uses LEGO's pretty printing facilities to adjust the line width of + the output." + (and (comint-check-proc (and proof-shell-process-name (proof-shell-buffer))) + (let ((current-width + (window-width (get-buffer-window proof-shell-buffer-name t)))) + (and (not (equal current-width + lego-shell-current-line-width)) + (progn + (setq lego-shell-current-line-width current-width) + (comint-simple-send lego-shell-process-name + (format lego-pretty-set-width + (- current-width 1)))))))) + +(defun lego-shell-zap-line-width () + (setq lego-shell-current-line-width nil)) + +(defun lego-shell-start-pp () + (cond (lego-pretty-p + (setq lego-shell-current-line-width nil) + (accept-process-output (get-process proof-shell-process-name)) + (proof-simple-send lego-pretty-on t) + (proof-simple-send lego-annotate-on t)))) + +(defun lego-shell-pre-shell-start () + (setq proof-shell-prog-name lego-shell-prog-name) + (setq proof-shell-process-name lego-shell-process-name) + (setq proof-shell-buffer-name (concat "*" lego-shell-process-name "*")) + (setq proof-shell-prompt-pattern lego-shell-prompt-pattern) + (setq proof-shell-mode-is 'lego-shell-mode) + (setq pbp-mode-is 'lego-pbp-mode) + (setq proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp) + (setq proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp) + (setq proof-shell-change-goal "Next %s;") + (setq proof-error-regexp lego-error-regexp) + (setq pbp-regexp-noise-goals-buffer "Discharge\\.\\. ") + (setq pbp-assumption-regexp lego-id) + (setq pbp-goal-regexp lego-goal-regexp) + (setq pbp-goals-buffer-name "*lego goals*")) +;; (Note that emacs can't cope with aliases to buffer local variables) + +(defun lego-shell-post-shell-start () + (lego-shell-start-pp) + (setq compilation-search-path (cons nil (lego-get-path))) + (add-hook 'proof-safe-send-hook 'lego-adjust-line-width) + (add-hook 'proof-shell-exit-hook 'lego-shell-zap-line-width) + (font-lock-fontify-buffer)) + + +(add-hook 'proof-pre-shell-start-hook 'lego-shell-pre-shell-start) +(add-hook 'proof-post-shell-start-hook 'lego-shell-post-shell-start) +;;;;;;;;;;;;;;;;;;;;;;; +;; Make support ;; +;;;;;;;;;;;;;;;;;;;;;;; + +(defvar lego-tmp-dir nil) + +(defun lego-module-name (file) + "Extract the name of the module from a file." + (substring (file-name-nondirectory file) 0 -2)) + +(defun lego-make-buffer () + "Save file then execute a Make command on it." + (interactive) + (and (buffer-modified-p) + (or (not lego-save-query) + (y-or-n-p (concat "Save file " + (buffer-file-name) + "? "))) + (save-buffer)) + (let ((module-name (lego-module-name buffer-file-name))) + (proof-simple-send (concat lego-make-command " " module-name ";") t))) + +(defun lego-make-buffer-until-point () + "Save from start of buffer until point, then run a Make" + (interactive) + (let ((file (concat lego-tmp-dir "/" + (lego-module-name buffer-file-name) ".l"))) + (write-region (point-min) (point) file) + (proof-simple-send + (concat lego-make-command " \"" file "\";") t))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-common-config () + +;; The following things *must* be set before proof-config-done + + (setq proof-terminal-char ?\;) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4") + + (proof-config-done) + + (define-key (current-local-map) "\M-\C-i" + (if (fboundp 'complete-tag) + 'complete-tag ; Emacs 19.31 (superior etags) + 'tag-complete-symbol)) ;XEmacs 19.13 (inferior etags) + (define-key (current-local-map) "\C-c\C-s" 'legogrep) + (define-key (current-local-map) "\C-c\C-p" 'lego-prf) + (define-key (current-local-map) "\C-ci" 'lego-intros) + (define-key (current-local-map) "\C-cI" 'lego-Intros) + (define-key (current-local-map) "\C-cr" 'lego-Refine) + (define-key (current-local-map) "\C-c\C-k" 'lego-killref) + (define-key (current-local-map) "\C-c\C-u" 'lego-undo-1) + (define-key (current-local-map) "\C-c\C-t" 'lego-restart-goal) + +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp lego-outline-regexp) + + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp lego-outline-heading-end-regexp) + +;; tags + (cond ((boundp 'tags-table-list) + (make-local-variable 'tags-table-list) + (setq tags-table-list (cons lego-tags tags-table-list)))) + + (and (boundp 'tag-table-alist) + (setq tag-table-alist + (append '(("\\.l$" . lego-tags) + ("lego" . lego-tags)) + tag-table-alist))) + + (setq font-lock-keywords lego-font-lock-keywords-1) + + (remove-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer t) + (add-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer nil t) + (remove-hook 'font-lock-mode-hook 'lego-fixup-change t) + (add-hook 'font-lock-mode-hook 'lego-fixup-change nil t) + + (font-lock-mode) + +) + + +(defun lego-mode-config () + + (lego-common-config) + +;; where to find files + + (setq compilation-search-path (cons nil (lego-get-path))) + (or lego-tmp-dir + (make-directory + (setq lego-tmp-dir (make-temp-name "/tmp/lego")))) + +;; keymaps and menus + (define-key lego-mode-map [(control c) (control b)] 'lego-make-buffer) + (define-key lego-mode-map [(control c) (control h)] + 'lego-make-buffer-until-point) + + (easy-menu-add lego-mode-menu lego-mode-map) + +;; font-lock + +;; if we don't have the following, zap-commas fails to work. + + (setq font-lock-always-fontify-immediately t) + +;; insert standard header and footer in fresh buffers + + (and (equal (buffer-size) 0) + buffer-file-name + (or (file-exists-p buffer-file-name) + (insert-before-markers + (format "Module %s;" (lego-module-name buffer-file-name)) + )))) + + +(defun lego-shell-mode-config () + + (lego-common-config) + + (easy-menu-add lego-shell-menu lego-shell-mode-map) + + (and running-xemacs (define-key lego-shell-mode-map + [button3] 'lego-shell-menu)) + + (setq font-lock-keywords lego-shell-font-lock-keywords-1) +) + +(defun lego-pbp-mode-config () + (lego-common-config) + (setq font-lock-keywords lego-font-lock-terms)) + +(provide 'lego) @@ -0,0 +1,300 @@ +;; pbp.el Major mode for proof by pointing +;; Subpackage of proof +;; Copyright (C) 1996 LFCS Edinburgh & INRIA Sophia Antipolis +;; Author: Yves Bertot < Yves.Bertot@sophia.inria.fr> +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; Time-stamp: <03 Mar 97 tms /home/tms/elisp/pbp.el> +;; Reference: Yves Bertot and Laurent Théry +;; A Generic Approach to Building User Interfaces for +;; Theorem Provers +;; J. Symbolic Computation (1996) +;; Accepted for Publication + +; The text structure is supposed to be given by annotations of the +; form %annotation text|annotated text@, The % and @ signs act as +; opening and closing parentheses, so that the annotated text may itself +; contain extra annotations. Analysing this structure yields the +; uncorrupted text (only "annotated text"), but the annotation are recorded +; into Emacs Extents that span over the text. + +;To construct these extents, one scans the whole text for the characters +; % and @. When finding a %, its location is simply kept on a stack +; *location-stack*. When finding a @, one looks in the stack to get +; the position of the last % and creates an extent with these two positions. +; The annotation is then removed and stored in the extent's properties +; and the last bits are cleared. + +(require 'proof) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Variables used by pbp, all auto-buffer-local ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(deflocal pbp-annotation-char ?@ "Annotation Mark") + +(deflocal pbp-goal-char ?g "goal mark") +(deflocal pbp-start-char ?s "annotation start") +(deflocal pbp-end-char ?e "annotation end") +(deflocal pbp-field-char ?x "annotated field end") + +(deflocal pbp-wakeup-character "\t" + "A character terminating the prompt in annotation mode") + +(deflocal pbp-assumption-regexp nil + "A regular expression matching the name of assumptions.") + +(deflocal pbp-goal-regexp nil + "A regular expressin matching the identifier of a goal.") + +(deflocal pbp-annotated-prompt-string "Lego> \t" + "Annotated prompt pattern") + +(deflocal pbp-start-goals-string "@s Start of Goals @e" + "String indicating the start of the proof state.") + +(deflocal pbp-end-goals-string "@s End of Goals @e" + "String indicating the end of the proof state.") + +(deflocal pbp-goal-command "Pbp %s %s;" + "Command informing the prover that `pbp-buttion-action' has been + requested on a goal. The first argument refers to the number of the + goal, the second to the path correpsonding to the selected subterm + of the goal.") + +(deflocal pbp-hyp-command "PbpHyp %s %s;" + "Command informing the prover that `pbp-buttion-action' has been + requested on an assumption. The first argument refers to the name of + the hypothesis, the second to the path corresponding to the selected + subterm of the assumption.") + +(deflocal pbp-result-start "@s Pbp result @e" + "String indicating the start of an output from the prover following + a `pbp-goal-command' or a `pbp-hyp-command'.") + +(deflocal pbp-result-end "@s End Pbp result @e" + "String indicating the end of an output from the prover following a + `pbp-goal-command' or a `pbp-hyp-command'.") + +(deflocal pbp-script-buffer nil + "The buffer in which commands corresponding to proof-by-pointing + actions will be recorded. The proof process is responsible for + updating this variable") + +(deflocal pbp-goals-buffer-name nil + "The name of the buffer in which goals are displayed in pbp mode") + +(deflocal pbp-goals-buffer nil + "The buffer in which goals are displayed in pbp mode") + +(deflocal pbp-regexp-noise-goals-buffer nil + "Unwanted information output from the proof process within + `pbp-start-goals-string' and `pbp-end-goals-string'.") + +(deflocal pbp-keymap (make-keymap 'Pbp-keymap) + "Keymap for pbp mode") + +(define-key pbp-keymap 'button2 'pbp-button-action) + +(deflocal pbp-mode-is nil + "The actual mode for Proof-by-Pointing.") + +(defun pbp-make-top-extent (start end) + (let (extent name) + (goto-char start) + (setq name (cond ((looking-at pbp-goal-regexp) + (cons 'goal (match-string 1))) + ((looking-at pbp-assumption-regexp) + (cons 'hyp (match-string 1))))) + (beginning-of-line) + (setq start (point)) + (goto-char end) + (beginning-of-line) + (backward-char) + (setq extent (make-extent start (point))) + (set-extent-property extent 'mouse-face 'highlight) + (set-extent-property extent 'keymap pbp-keymap) + (set-extent-property extent 'pbp-top-element name))) + +(defun pbp-analyse-structure (string) + (save-excursion + (let* ((ip 0) (op 0) (l (length string)) (stack ()) (topl ()) ext n + (out (make-string l ?x )) ) + (while (< ip l) + (if (not (char-equal (aref string ip) pbp-annotation-char)) + (progn (aset out op (aref string ip)) + (setq op (+ 1 op))) + (setq ip (+ 1 ip)) + (cond + ((char-equal (aref string ip) pbp-goal-char) + (setq topl (append topl (list (+ 1 op)) ))) + ((char-equal (aref string ip) pbp-start-char) + (setq n (setq ip (+ 1 ip))) + (while (not (char-equal (aref string ip) pbp-annotation-char)) + (setq ip (+ 1 ip))) + (setq stack (cons op (cons (substring string n ip) stack))) + (setq ip (+ 1 ip))) + ((char-equal (aref string ip) pbp-field-char) + (setq ext (make-extent (car stack) op out)) + (set-extent-property ext 'mouse-face 'highlight) + (set-extent-property ext 'keymap pbp-keymap) + (set-extent-property ext 'pbp (cadr stack)) + (set-extent-property ext 'duplicable t) + (setq stack (cddr stack))))) + (setq ip (+ 1 ip))) + + (pop-to-buffer pbp-goals-buffer) + (erase-buffer) + (insert (substring out 0 op)) + (while (setq ip (car topl) + topl (cdr topl)) + (pbp-make-top-extent ip (car topl))) + (pbp-make-top-extent ip (point-max))))) + +; Receiving the data from Lego is performed that a filter function +; added among the comint-output-filter-functions of the shell-mode. + +(deflocal pbp-mark-ext nil "last mark") +(deflocal pbp-sanitise t "sanitise output?") + +(defun pbp-sanitise-string (string) + (if pbp-sanitise + (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) + (while (< ip l) + (if (char-equal (aref string ip) pbp-annotation-char) + (if (char-equal (aref string (setq ip (+ 1 ip))) + pbp-start-char) + (progn + (while (not (char-equal (aref string ip) + pbp-annotation-char)) + (setq ip (+ 1 ip))) + (setq ip (+ 1 ip)))) + (aset out op (aref string ip)) + (setq op (+ 1 op))) + (setq ip (+ 1 ip))) + (substring out 0 op)) + string)) + +(defun pbp-display-error (string) + (save-excursion + (pop-to-buffer pbp-goals-buffer) + (goto-char (point-max)) + (if (re-search-backward proof-error-regexp nil t) + (delete-region (- (point) 2) (point-max))) + (newline 2) + (let ((start (point))) + (insert-string string) + + ;; tms - I don't really understand what this is doing, but omitting it + ;; will not give any fontification via font-lock + (font-lock-fontify-syntactically-region start (point-max)) + + ;; display complete region in red + (put-nonduplicable-text-property start (point-max) + 'face font-lock-error-face) + ;; fontify according to the appropriate font-lock table + (font-lock-fontify-keywords-region start (point-max))))) + +(defun pbp-send-and-remember (string) + (save-excursion + (proof-simple-send string) + (if (and (boundp 'pbp-script-buffer) pbp-script-buffer) + (progn (set-buffer pbp-script-buffer) + (end-of-buffer) + (insert-string string))))) + +(defun pbp-process-string (string) + + (let (start end) + (save-excursion + (cond + ((string-match proof-error-regexp string) + (pbp-display-error + (pbp-sanitise-string (substring string (match-beginning 0))))) + + ((string-match proof-shell-abort-goal-regexp string) + (erase-buffer pbp-goals-buffer)) + + ((string-match proof-shell-proof-completed-regexp string) + (erase-buffer pbp-goals-buffer) + (insert-string (concat "\n" (match-string 0 string)) pbp-goals-buffer)) + + ((string-match pbp-start-goals-string string) + (while (progn (setq start (match-end 0)) + (string-match pbp-start-goals-string string start))) + (string-match pbp-end-goals-string string start) + (setq end (match-beginning 0)) + (pbp-analyse-structure (substring string start end))) + + ((string-match pbp-result-start string) + (setq start (+ 1 (match-end 0))) + (string-match pbp-result-end string) + (setq end (- (match-beginning 0) 1)) + (pbp-send-and-remember (substring string start end))))))) + +(defun pbp-filter (str) + (if (string-match pbp-wakeup-character str) + (save-excursion + (set-buffer (proof-shell-buffer)) + (let (string mrk) + (while (progn (goto-char (extent-start-position pbp-mark-ext)) + (setq mrk (point-marker)) + (search-forward pbp-annotated-prompt-string nil t)) + (set-extent-endpoints pbp-mark-ext (point) (point)) + (backward-char (length pbp-annotated-prompt-string)) + (setq string (buffer-substring mrk (point))) + (delete-region mrk (point)) + (insert (pbp-sanitise-string string)) + (goto-char (extent-start-position pbp-mark-ext)) + (backward-delete-char 1) + (pbp-process-string string)))))) + +; Call after the shell is started + +(defun pbp-goals-init () + (save-excursion + (setq pbp-goals-buffer (get-buffer-create pbp-goals-buffer-name )) + (set-buffer pbp-goals-buffer) + (funcall pbp-mode-is) + (erase-buffer pbp-goals-buffer) + (add-hook 'comint-output-filter-functions 'pbp-filter t) + (set-buffer (proof-shell-buffer)) + (setq pbp-mark-ext (make-extent (point-max) (point-max))) + (set-extent-property pbp-mark-ext 'detachable nil) + (set-extent-property pbp-mark-ext 'start-open nil) + (set-extent-property pbp-mark-ext 'end-open t) + (add-hook 'proof-shell-exit-hook + (lambda () + (remove-hook 'comint-output-filter-functions 'pbp-filter))))) + +; Now, using the extents in a mouse behavior is quite simple: +; from the mouse position, find the relevant extent, then get its annotation +; and produce a piece of text that will be inserted in the right buffer. +; Attaching this behavior to the mouse is simply done by attaching a keymap +; to all the extents. + + +(defun pbp-button-action (event) + (interactive "e") + (mouse-set-point event) + (pbp-construct-command)) + + +(defun pbp-construct-command () + (let ((ext (extent-at (point) () 'pbp)) + (top-ext (extent-at (point) () 'pbp-top-element))) + + (cond ((extentp top-ext) + (let* ((top-info (extent-property top-ext 'pbp-top-element)) + (path (if (extentp ext) + (extent-property ext 'pbp) "")) + (command (if (eq 'hyp (car top-info)) + pbp-hyp-command pbp-goal-command))) + (proof-command + (format command (cdr top-info) path))))))) + + + +(define-derived-mode pbp-mode fundamental-mode "Pbp" "Proof by Pointing" + (suppress-keymap pbp-mode-map)) + +(provide 'pbp) diff --git a/proof.el b/proof.el new file mode 100644 index 00000000..086998b1 --- /dev/null +++ b/proof.el @@ -0,0 +1,546 @@ +;; proof.el Major mode for proof assistants Copyright (C) 1994, +;; 1995, 1996 LFCS Edinburgh. This version by Dilip Sequeira, by +;; rearranging Thomas Schreiber's code. + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; Time-stamp: <22 Nov 96 tms /home/tms/elisp/proof.el> +;; Thanks to David Aspinall, Robert Boyer, Rod Burstall, +;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens + + +(require 'compile) +(require 'comint) +(require 'etags) + +(autoload 'w3-fetch "w3" nil t) +(autoload 'easy-menu-define "easymenu") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuration ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-echo-input t + "If nil, input to the proof shell will not be echoed") + +(defvar proof-prog-name-ask-p nil + "*If t, you will be asked which program to run when the inferior + process starts up.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Variables used by proof mode, all auto-buffer-local ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmacro deflocal (var &optional value docstring) + (list 'make-variable-buffer-local (list 'quote var)) + (list 'defvar var value docstring)) + +;; These should be set before proof-config-done is called + +(deflocal proof-terminal-char) + +(make-local-hook 'proof-pre-shell-start-hook) +(make-local-hook 'proof-post-shell-start-hook) + +(deflocal proof-comment-start) +(deflocal proof-comment-end) + +;; these should be set in proof-shell-start-hook + +(deflocal proof-shell-prog-name) +(deflocal proof-shell-process-name) +(deflocal proof-shell-buffer-name) +(deflocal proof-shell-prompt-pattern) +(deflocal proof-shell-mode-is) + +(deflocal proof-shell-abort-goal-regexp nil + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(deflocal proof-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +(deflocal proof-shell-proof-completed-regexp nil + "*Regular expression indicating that the proof has been completed.") + +(deflocal proof-shell-change-goal nil + "*Command to change to the goal %s") + +;; Supply these if you want + +(make-local-hook 'proof-shell-safe-send-hook) +(make-local-hook 'proof-shell-exit-hook) + +;; These get computed in proof-mode-child-config-done + +(deflocal proof-terminal-string) +(deflocal proof-re-end-of-cmd) +(deflocal proof-re-term-or-comment) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar running-xemacs nil) +(defvar running-emacs19 nil) + +(setq running-xemacs (string-match "XEmacs\\|Lucid" emacs-version)) +(or running-xemacs + (setq running-emacs19 (string-match "^19\\." emacs-version))) + +;; courtesy of Mark Ruys +(defun emacs-version-at-least (major minor) + "Test if emacs version is at least major.minor" + (or (> emacs-major-version major) + (and (= emacs-major-version major) (>= emacs-minor-version minor))) +) + +(defvar extended-shell-command-on-region + (emacs-version-at-least 19 29) + "Does `shell-command-on-region' optionally offer to output in an other buffer?") + +;; in case Emacs is not aware of read-shell-command-map +(defvar read-shell-command-map + (let ((map (make-sparse-keymap))) + (if (not (fboundp 'set-keymap-parents)) + (setq map (append minibuffer-local-map map)) + (set-keymap-parents map minibuffer-local-map) + (set-keymap-name map 'read-shell-command-map)) + (define-key map "\t" 'comint-dynamic-complete) + (define-key map "\M-\t" 'comint-dynamic-complete) + (define-key map "\M-?" 'comint-dynamic-list-completions) + map) + "Minibuffer keymap used by shell-command and related commands.") + + +;; in case Emacs is not aware of the function read-shell-command +(or (fboundp 'read-shell-command) + ;; from minibuf.el distributed with XEmacs 19.11 + (defun read-shell-command (prompt &optional initial-input history) + "Just like read-string, but uses read-shell-command-map: +\\{read-shell-command-map}" + (let ((minibuffer-completion-table nil)) + (read-from-minibuffer prompt initial-input read-shell-command-map + nil (or history + 'shell-command-history))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A couple of small utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun string-to-list (s separator) + "converts strings `s' separated by the character `separator' to a + list of words" + (let ((end-of-word-occurence (string-match (concat separator "+") s))) + (if (not end-of-word-occurence) + (if (string= s "") + nil + (list s)) + (cons (substring s 0 end-of-word-occurence) + (string-to-list + (substring s + (string-match (concat "[^" separator "]") + s end-of-word-occurence)) separator))))) + + + +(defun ids-to-regexp (l) + "transforms a non-empty list of identifiers `l' into a regular + expression matching any of its elements" +(mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) + +(defun w3-remove-file-name (address) + "remove the file name in a World Wide Web address" + (string-match "://[^/]+/" address) + (concat (substring address 0 (match-end 0)) + (file-name-directory (substring address (match-end 0))))) + +(defun occurence (STRING &optional LOWER-BOUND UPPER-BOUND) + "Counts the number of occurences of STRING in the current buffer + between the positions LOWER-BOUND and UPPER-BOUND. + Optional first argument. nil is equivalent to (point-min). + Optional second argument. nil is equivalent to (point-max)." + (save-excursion + (let ((LOWER-BOUND (or LOWER-BOUND (point-min)))) + (goto-char LOWER-BOUND) + (let ((pos (search-forward STRING UPPER-BOUND t))) + (if pos (+ 1 (occurence STRING pos UPPER-BOUND)) 0))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A few random hacks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-skip-comments () + (forward-comment (buffer-size)) + (point)) + +; Find the last real semicolon, or point-min, leaving the point after +; the semi and any junk. Returns nil if we seemto be inside a comment + +(defun proof-find-start-of-command () + (if (re-search-backward proof-re-term-or-comment nil t) + (cond ((looking-at proof-terminal-string) + (forward-char) + (proof-skip-comments)) + ((looking-at (substring proof-comment-start 0 1)) nil) + ((looking-at (substring proof-comment-end 0 1)) + (if (search-backward proof-comment-start nil t) + (if (equal (point) (point-min)) + (proof-skip-comments)) + (backward-char) + (proof-find-start-of-command)) + (point))) + (goto-char (point-min)) + (proof-skip-comments))) + + +;; there seems to be some duplication of work here, as one might +;; expect that the functionality of proof-find-end-of-command would be +;; required in proof-process-active-terminator +(defun proof-find-end-of-command (&optional COUNT) + "Move to the end of the command. COUNT-1 end-of-command symbols + `proof-terminal-string' are within comments" + (interactive) + (let ((point (point)) + (pos (search-forward proof-terminal-string nil nil COUNT))) + (and pos + ;; an end of command has been found + ;; is pos within a comment relative to the starting point of + ;; the search? + (> (occurence proof-comment-start point (point)) + (occurence proof-comment-end point (point))) + (goto-char point) + (proof-find-end-of-command (if COUNT (+ 1 COUNT) 2))))) + +(defun proof-shell-process () + (and (stringp proof-shell-process-name) + (get-process proof-shell-process-name))) + +(defun proof-shell-buffer () + (and (stringp proof-shell-buffer-name) + (get-buffer proof-shell-buffer-name))) + +(defun proof-display-buffer (buffer) + (let ((tmp-buffer (current-buffer))) + (display-buffer buffer) + (display-buffer tmp-buffer))) + +(defun proof-append-terminator (string) + (or (and + (string-match proof-re-end-of-cmd string) + string) + (setq string (concat string proof-terminal-string)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Comint-style stuff: sending input to the process etc ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-input-sender (proc string) + "Function to actually send to the PROOF process `proc' the `string' + submitted by the user. It then calls proof-shell-safe-send-hook if safe + to do so." + (comint-simple-send proc string) + (and (string-match proof-re-end-of-cmd string) + (run-hooks 'proof-shell-safe-send-hook))) + +(defun proof-interrupt-subjob () + (interactive) + (and (proof-shell-process) + (interrupt-process (proof-shell-process)))) + +(defun proof-simple-send (string &optional silent) + "send `string' to the PROOF PROCESS. + If `silent' is enabled then `string' should not be echoed." + (or (proof-shell-process) (proof-start-shell)) + (let ((proof-buf (proof-shell-buffer))) + (if proof-buf + (save-excursion + (progn + (set-buffer proof-buf) + (goto-char (point-max)) + (if (and proof-shell-echo-input (not silent)) + (progn + (princ string proof-buf) + (comint-send-input)) + (proof-input-sender proof-shell-process-name string) + ))) + (message (format "No active %s process" proof-shell-process-name))))) + +(defun proof-simulate-send-region (point1 point2 &optional terminator) + "Send the area between point1 and point2 to the inferior shell running lego." + (let (str) + (setq str (buffer-substring point1 point2)) + (and terminator (setq str (proof-append-terminator str))) + (proof-simple-send str))) + +;; proof-send-command tries to figure out where commands start and end +;; without having to parse expressions. Actually needs re-writing. + +(defun proof-send-command () + "Send current command to inferior shell." + + (interactive) + (let (start end) + (save-excursion + (setq start (proof-find-start-of-command)) + (if start + (setq end (search-forward proof-terminal-string nil t))) + (if (not end) + (setq end (point-max)) + (backward-char)) + (proof-simulate-send-region start end t)))) + +(defun proof-send-line () + "Send current line to inferior shell running proof" + (interactive) + (save-excursion + (let (start end) + (beginning-of-line 1) + (setq start (point)) + (end-of-line 1) + (setq end (point)) + (proof-simulate-send-region start end))) + (forward-line 1)) + +(defun proof-send-region () + "Sends the current region to the inferior shell running proof and + appends a terminator if neccessary." + (interactive) + (let (start end) + (save-excursion + (setq end (point)) + (exchange-point-and-mark) + (setq start (point))) + (proof-simulate-send-region start end t))) + +(defun proof-command (command &optional silent) + (let ((str (proof-append-terminator command))) + (proof-simple-send str silent))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Starting, stopping, and interrupting the lego shell ;; +;; There maybe more functionality here one day to support multiple ;; +;; subprocesses ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-start-shell () + (run-hooks 'proof-pre-shell-start-hook) + (let ((proof-buf (and proof-shell-process-name (proof-shell-buffer)))) + (if (comint-check-proc proof-buf) + () + (save-excursion + (and proof-prog-name-ask-p + (setq proof-shell-prog-name + (read-shell-command "Run process: " + proof-shell-prog-name)))) + (or proof-shell-process-name + (setq proof-shell-process-name + (concat + "Inferior " + (substring proof-shell-prog-name + (string-match "[^/]*$" proof-shell-prog-name) + (string-match "$" proof-shell-prog-name))))) + (message (format "Starting %s process..." proof-shell-process-name)) + + (proof-spawn-process proof-shell-prog-name + proof-shell-process-name proof-shell-buffer-name) + (run-hooks 'proof-post-shell-start-hook) + (pbp-goals-init) + (message + (format "Starting %s process... done." proof-shell-process-name))))) + + +(defun proof-spawn-process (prog-name process-name buffer-name) + "Start a new shell in a new buffer" + + (set-buffer + (let ((prog-name-list (string-to-list prog-name " "))) + (apply 'make-comint + (append (list process-name + (car prog-name-list) nil) + (cdr prog-name-list))))) + + (erase-buffer) + (funcall proof-shell-mode-is) + (setq comint-prompt-regexp proof-shell-prompt-pattern) + (setq comint-input-sender 'proof-input-sender) + (and running-emacs19 (setq comint-scroll-show-maximum-output t)) + (proof-display-buffer buffer-name) + (set-buffer buffer-name) + ) + +(defun proof-shell-exit () + "Exit the PROOF process + + Runs proof-shell-exit-hook if non nil" + + (interactive) + (save-excursion + (let ((buffer (proof-shell-buffer))) + (and buffer + (progn + (save-excursion + (set-buffer buffer) + (comint-send-eof)) + (kill-buffer buffer) + + (run-hooks 'proof-shell-exit-hook) + + ;;it is important that the hooks are + ;;run after the buffer has been killed. In the reverse + ;;order e.g., intall-shell-fonts causes problems and it + ;;is impossilbe to restart the PROOF shell + + (message + (format "%s process terminated." proof-shell-process-name))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Active terminator minor mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-active-terminator-minor-mode nil) +(make-variable-buffer-local 'proof-active-terminator-minor-mode) +(put 'proof-active-terminator-minor-mode 'permanent-local t) + +(defun proof-active-terminator-minor-mode (&optional arg) + "Toggle PROOF's Active Terminator minor mode. +With arg, turn on the Active Terminator minor mode if and only if arg +is positive. + +If Active terminator mode is enabled, a terminator will process the +current command." + + (interactive "P") + +;; has this minor mode been registered as such? + (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-terminator-minor-mode " ;"))))) + + (setq proof-active-terminator-minor-mode + (if (null arg) (not proof-active-terminator-minor-mode) + (> (prefix-numeric-value arg) 0))) + (if (fboundp 'redraw-modeline) (redraw-modeline) (force-mode-line-update))) + +(defun proof-active-terminator () + (interactive) + (if proof-active-terminator-minor-mode + (proof-process-active-terminator) + (self-insert-command 1))) + +(defun proof-process-active-terminator () + "Process an active terminator key-press" + + (interactive) + (let (start) + (and (re-search-backward "[^ ]" nil t) + (not (char-equal (following-char) proof-terminal-char)) + (forward-char)) + (save-excursion + (setq start (proof-find-start-of-command))) + (if (not start) + (self-insert-command 1) + (if (> start (point)) + (setq start (point))) + (proof-simulate-send-region start (point) t) + (if (char-equal proof-terminal-char (following-char)) + (forward-char) + (self-insert-command 1))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar font-lock-declaration-name-face +(progn + (cond ((x-display-color-p) + ;notice that device-class does not exist in Emacs 19.30 + + (copy-face 'bold 'font-lock-declaration-name-face) + + ;; Emacs 19.28 compiles this down to + ;; internal-set-face-1. This is not compatible with XEmacs + (dont-compile + (set-face-foreground + 'font-lock-declaration-name-face "chocolate"))) + (t (copy-face 'bold-italic 'font-lock-declaration-name-face))) + (if running-emacs19 + (setq font-lock-declaration-name-face + (face-name 'font-lock-declaration-name-face))))) + +(defvar font-lock-tacticals-name-face +(if (x-display-color-p) + (let ((face (make-face 'font-lock-tacticals-name-face))) + (dont-compile + (set-face-foreground face + "MediumOrchid3")) + face) + (copy-face 'bold 'font-lock-tacticals-name-face))) + +(defvar font-lock-error-face +(if (x-display-color-p) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face + "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode configuration ;; +;; Eventually there will be some more ;; +;; functionality here common to both coq and lego. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(define-derived-mode proof-mode fundamental-mode + "Proof" "Proof mode - not standalone" + ()) + +(define-key proof-mode-map [(control c) (control e)] + 'proof-find-end-of-command) +(define-key proof-mode-map [(control c) (control j)] 'proof-send-line) +(define-key proof-mode-map [(control c) (control r)] 'proof-send-region) +(define-key proof-mode-map [(control c) (control c)] 'proof-interrupt-subjob) + +(define-derived-mode proof-shell-mode comint-mode + "proof-shell" "Proof shell mode - not standalone" + ()) + +;; the following callback is an irritating hack - there should be some +;; elegant mechanism for computing constants after the child has +;; configured. + +(defun proof-config-done () + +;; calculate some strings and regexps for searching + + (setq proof-terminal-string (char-to-string proof-terminal-char)) + + (make-local-variable 'comment-start) + (setq comment-start (concat proof-comment-start " ")) + (make-local-variable 'comment-end) + (setq comment-end (concat " " proof-comment-end)) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip + (concat (regexp-quote proof-comment-start) "+\\s_?")) + + (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'")) + (setq proof-re-term-or-comment + (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) + "\\|" (regexp-quote proof-comment-end))) + + (define-key proof-mode-map + (vconcat [(control c)] (vector proof-terminal-char)) + 'proof-active-terminator-minor-mode) + + (define-key proof-mode-map proof-terminal-char 'proof-active-terminator) + + ) + + +(provide 'proof) |