;; isa.el Major mode for Isabelle proof assistant ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; ;; Author: David Aspinall ;; Maintainer: Proof General maintainer ;; ;; $Id$ ;; ;; Add Isabelle image onto splash screen (customize-set-variable 'proof-splash-extensions '(list nil (proof-splash-display-image "isabelle_transparent" t))) (require 'proof) (require 'isa-syntax) ;; To make byte compiler be quiet. ;; NASTY: these result in loads when evaluated ;; ordinarily (from non-byte compiled code). ;(eval-when-compile ; (require 'proof-script) ; (require 'proof-shell) ; (require 'outline) ; (cond ((fboundp 'make-extent) (require 'span-extent)) ; ((fboundp 'make-overlay) (require 'span-overlay)))) ;;; variable: proof-analyse-using-stack ;;; proof-locked-region-empty-p, proof-shell-insert, pbp-mode, ;;; proof-complete-buffer-atomic, proof-shell-invisible-command, ;;; prev-span, span-property, next-span, proof-unprocessed-begin, ;;; proof-config-done, proof-shell-config-done ;;; ;;; ======== User settings for Isabelle ======== ;;; ;;; proof-site provides us with the cusomization groups ;;; ;;; 'isabelle - User options for Isabelle Proof General ;;; 'isabelle-config - Configuration of Isabelle Proof General ;;; (constants, but may be nice to tweak) (defcustom isabelle-prog-name "isabelle" "*Name of program to run Isabelle." :type 'file :group 'isabelle) (defcustom isabelle-indent 2 "*Indentation degree in proof scripts. Somewhat irrelevant for Isabelle because normal proof scripts have no regular or easily discernable structure." :type 'number :group 'isabelle) (defcustom isabelle-web-page "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html" ;; "http://www.dcs.ed.ac.uk/home/isabelle" "URL of web page for Isabelle." :type 'string :group 'isabelle) ;;; ;;; ======== Configuration of generic modes ======== ;;; ;; ===== outline mode ;;; FIXME: test and add more things here (defcustom isa-outline-regexp (proof-ids-to-regexp '("goal" "Goal" "prove_goal")) "Outline regexp for Isabelle ML files" :type 'regexp :group 'isabelle-config) ;;; End of a command needs parsing to find, so this is approximate. (defcustom isa-outline-heading-end-regexp ";[ \t\n]*" "Outline heading end regexp for Isabelle ML files." :type 'regexp :group 'isabelle-config) ;; FIXME: not sure about this one (defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.") (defvar isa-shell-outline-heading-end-regexp "$") ;;; ---- end-outline ;;; NB! Disadvantage of *not* shadowing variables is that user ;;; cannot override them. It might be nice to override some ;;; variables, which ones? (defun isa-mode-config-set-variables () "Configure generic proof scripting/thy mode variables for Isabelle. Settings here are the ones which are needed for both shell mode and script mode." (setq proof-assistant-home-page isabelle-web-page proof-mode-for-script 'isa-proofscript-mode ;; proof script syntax proof-terminal-char ?\; ; ends a proof proof-comment-start "(*" ; comment in a proof proof-comment-end "*)" ; ;; Next few used for func-menu and recognizing goal..save regions in ;; script buffer. proof-save-command-regexp isa-save-command-regexp proof-goal-command-regexp isa-goal-command-regexp proof-goal-with-hole-regexp isa-goal-with-hole-regexp proof-save-with-hole-regexp isa-save-with-hole-regexp ;; Unfortunately the default value of proof-script-next-entity-regexps ;; is no good, because goals with holes in Isabelle are batch ;; commands, and not terminated by saves. So we omit the forward ;; search from the default value. proof-script-next-entity-regexps (list (proof-regexp-alt isa-goal-with-hole-regexp isa-save-with-hole-regexp) (list isa-goal-with-hole-regexp 2) (list isa-save-with-hole-regexp 2 'backward isa-goal-command-regexp)) ;; proof-indent-commands-regexp (proof-ids-to-regexp isa-keywords) ;; proof engine commands proof-showproof-command "pr()" proof-goal-command "Goal \"%s\";" proof-save-command "qed \"%s\";" proof-context-command "ProofGeneral.show_context()" proof-info-command "ProofGeneral.help()" proof-kill-goal-command "ProofGeneral.kill_goal();" proof-find-theorems-command "ProofGeneral.thms_containing [\"%s\"]" ;; command hooks proof-goal-command-p 'isa-goal-command-p proof-count-undos-fn 'isa-count-undos proof-find-and-forget-fn 'isa-find-and-forget proof-goal-hyp-fn 'isa-goal-hyp proof-state-preserving-p 'isa-state-preserving-p proof-parse-indent 'isa-parse-indent proof-stack-to-indent 'isa-stack-to-indent ;; close goal..save regions eagerly proof-completed-proof-behaviour 'closeany proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";" proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";")) (defun isa-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle." (setq proof-shell-first-special-char ?\350 proof-shell-wakeup-char ?\372 proof-shell-annotated-prompt-regexp "\\(val it = () : unit\n\\)?> \372" ;; "^\\(val it = () : unit\n\\)?> " ;; non-annotation, with val it's: "^\\(val it = () : unit\n\\)?> " ;; This pattern is just for comint, it matches a range of ;; prompts from a range of MLs, including Isabelle's edited ;; version. proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?" ;; for issuing command, not used to track cwd in any way. proof-shell-cd-cmd "cd \"%s\"" ;; FIXME: the next two are probably only good for NJ/SML proof-shell-interrupt-regexp "Interrupt" proof-shell-error-regexp "^\364\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " ;; matches names of assumptions proof-shell-assumption-regexp isa-id ;; matches subgoal name ;; FIXME: proof-shell-goal-regexp is *not* used at the generic level! ;; Perhaps it should be renamed to isa-goal-regexp and be ;; set somewhere else. proof-shell-goal-regexp "\370[ \t]*\\([0-9]+\\)\\." proof-shell-start-goals-regexp "\366" proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 proof-shell-proof-completed-regexp (concat proof-shell-start-goals-regexp "\\(\\(.\\|\n\\)*\nNo subgoals!\n\\)" proof-shell-end-goals-regexp) ;; initial command configures Isabelle by hacking print functions. proof-shell-init-cmd "ProofGeneral.init false;" proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-end "\361\\|\363" ;; Some messages delimited by eager annotations proof-shell-clear-response-regexp "Proof General, please clear the response buffer." proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." ;; Tested values of proof-shell-eager-annotation-start: ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading" ;; "^---\\|^\\[opening " ;; could be last bracket on end of line, or with ### and ***. ;; Dirty hack to allow font-locking for output based on hidden ;; annotations, see isa-output-font-lock-keywords-1 proof-shell-leave-annotations-in-output t proof-goals-display-qed-message t ;; === ANNOTATIONS === ones here are broken proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" proof-analyse-using-stack t proof-shell-start-char ?\372 proof-shell-end-char ?\373 proof-shell-field-char ?\374 ;; === MULTIPLE FILE HANDLING === proof-shell-process-file (cons ;; Theory loader output and verbose update() output. "Proof General, this file is loaded: \"\\(.*\\)\"" (lambda (str) (match-string 1 str))) ;; \\|Not reading \"\\(.*\\)\" ;; (lambda (str) ;; (or (match-string 1 str) ;; (match-string 2 str)))) ;; This is the output returned by a special command to ;; query Isabelle for outdated files. ;; proof-shell-clear-included-files-regexp ;; "Proof General, please clear your record of loaded files." proof-shell-retract-files-regexp "Proof General, you can unlock the file \"\\(.*\\)\"" proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list ) (add-hook 'proof-activate-scripting-hook 'isa-shell-update-thy 'append) ) ;;; ;;; Theory loader operations ;;; (defun isa-update-thy-only (file try wait) "Tell Isabelle to update current buffer's theory, and all ancestors." (proof-shell-invisible-command (format "ProofGeneral.%supdate_thy_only \"%s\";" (if try "try_" "") (file-name-sans-extension file)) wait)) ;; Experiments for background non-blocking loading of theory: this is ;; quite difficult, actually: we need to set a callback from ;; proof-done-invisible to take the final step in switching on ;; scripting. We may be able to pass the hook argument into the ;; action list using the "span" argument which means nothing for ;; invisible command usually. ;(defun isa-update-error (&rest args) ; "Callback for proof-invisible-command. ;In case an update leads to an error/interrupt in Isabelle, ;we make sure scripting is deactivated and raise an elisp error." ; (if proof-shell-error-or-interrupt-seen ; (proof-deactivate-scripting)) ; (proof-shell-done-invisible "Isabelle Proof General: error during use_thy, scripting not activated!")) (defun isa-shell-update-thy () "Possibly issue update_thy_only command to Isabelle. If the current buffer has an empty locked region, the interface is about to send commands from it to Isabelle. This function sends a command to read any theory file corresponding to the current ML file. This is a hook function for proof-activate-scripting-hook." (if (proof-locked-region-empty-p) ;; If we switch to this buffer and it *does* have a locked ;; region, we could check that no updates are needed and ;; unlock the whole buffer in case they were. But that's ;; a bit messy. Instead we assume that things must be ;; up to date, after all, the user wasn't allowed to edit ;; anything that this file depends on, was she? (progn ;; Wait after sending, so that queue is cleared ;; for further commands without giving "proof process ;; busy" error. (isa-update-thy-only buffer-file-name t ;; whether to block or not (if (and (boundp 'activated-interactively) activated-interactively) t ; was nil, but will falsely leave Scripting on! t)) ;; Leave the messages from the update around. (setq proof-shell-erase-response-flag nil)))) (defun isa-remove-file (name files cmp-base) (if (not files) nil (let* ((file (car files)) (rest (cdr files)) (same (if cmp-base (string= name (file-name-nondirectory file)) (string= name file)))) (if same (isa-remove-file name rest cmp-base) (cons file (isa-remove-file name rest cmp-base)))))) (defun isa-shell-compute-new-files-list (str) "Compute the new list of files read by the proof assistant. This is called when Proof General spots output matching proof-shell-retract-files-regexp." (let* ((name (match-string 1 str)) (base-name (file-name-nondirectory name))) (if (string= name base-name) (isa-remove-file name proof-included-files-list t) (isa-remove-file (file-truename name) proof-included-files-list nil)))) ;; ;; Define the derived modes ;; (eval-and-compile (define-derived-mode isa-shell-mode proof-shell-mode "Isabelle shell" nil (isa-shell-mode-config))) (eval-and-compile (define-derived-mode isa-response-mode proof-response-mode "Isabelle response" nil (isa-response-mode-config))) (eval-and-compile ; to define vars for byte comp. (define-derived-mode isa-pbp-mode pbp-mode "Isabelle goals" nil (isa-pbp-mode-config))) (eval-and-compile ; to define vars for byte comp. (define-derived-mode isa-proofscript-mode proof-mode "Isabelle script" nil (isa-mode-config))) ; (define-key isa-proofscript-mode-map ; [(control c) (control l)] 'proof-prf) ; keybinding like Isamode ;; Automatically selecting theory mode or Proof General script mode. (defun isa-mode () "Mode for Isabelle buffers: either isa-proofscript-mode or thy-mode. Files with extension .thy will be in thy-mode, otherwise we choose isa-proofscript-mode." (interactive) (cond (;; Theory files only if they have the right extension (and (buffer-file-name) (string-match "\\.thy$" (buffer-file-name))) ;; Enter theory mode, but first configure settings for proof ;; script if they haven't been done already. This is a hack, ;; needed because Proof General assumes that the script mode must ;; have been configured before shell mode can be triggered, which ;; isn't true for Isabelle. ;; (proof-config-done-related and proof-shell-mode refer to ;; the troublesome settings in question) (unless proof-terminal-char (isa-mode-config-set-variables)) (thy-mode) ;; related mode configuration including locking buffer. (proof-config-done-related) ;; Hack for splash screen (if (and (boundp 'proof-mode-hook) (memq 'proof-splash-timeout-waiter proof-mode-hook)) (proof-splash-timeout-waiter) ;; Otherwise, user may need welcoming. (proof-splash-message))) (t (isa-proofscript-mode)))) (eval-after-load "thy-mode" ;; Extend theory mode keymap '(let ((map thy-mode-map)) (define-key map "\C-c\C-b" 'isa-process-thy-file) (define-key map "\C-c\C-r" 'isa-retract-thy-file))) ;; FIXME: could test that the buffer isn't already locked. (defun isa-process-thy-file (file) "Process the theory file FILE. If interactive, use buffer-file-name." (interactive (list buffer-file-name)) (save-some-buffers) (isa-update-thy-only file nil nil)) (defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%s\";" "Sent to Isabelle to forget theory file and descendants. Resulting output from Isabelle will be parsed by Proof General." :type 'string :group 'isabelle-config) (defun isa-retract-thy-file (file) "Retract the theory file FILE. If interactive, use buffer-file-name. To prevent inconsistencies, scripting is deactivated before doing this. So if scripting is active in an ML file which is not completely processed, you will be asked to retract the file or process the remainder of it. (If you process the rest of it it may subsequently be unlocked anyway). " (interactive (list buffer-file-name)) (proof-deactivate-scripting) (proof-shell-invisible-command (format isa-retract-thy-file-command (file-name-nondirectory (file-name-sans-extension file))))) ;; Next bits taken from isa-load.el ;; isa-load.el,v 3.8 1998/09/01 (defgroup thy nil "Customization of Isamode's theory editing mode" ;; :link '(info-link "(Isamode)Theory Files") :load 'thy-mode :group 'isabelle) (autoload 'thy-mode "thy-mode" "Major mode for Isabelle theory files" t nil) (autoload 'thy-find-other-file "thy-mode" "Find associated .ML or .thy file." t nil) (defun isa-splice-separator (sep strings) (let (stringsep) (while strings (setq stringsep (concat stringsep (car strings))) (setq strings (cdr strings)) (if strings (setq stringsep (concat stringsep sep)))) stringsep)) (defun isa-file-name-cons-extension (name) "Return cons cell of NAME without final extension and extension" (if (string-match "\\.[^\\.]+$" name) (cons (substring name 0 (match-beginning 0)) (substring name (match-beginning 0))) (cons name ""))) (defun isa-format (alist string) "Format a string by matching regexps in ALIST against STRING" (while alist (while (string-match (car (car alist)) string) (setq string (concat (substring string 0 (match-beginning 0)) (cdr (car alist)) (substring string (match-end 0))))) (setq alist (cdr alist))) string) ;; Key to switch to theory mode (define-key isa-proofscript-mode-map [(control c) (control o)] 'thy-find-other-file) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Code that's Isabelle specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; FIXME: think about the next variable. I've changed sense from ;; LEGO and Coq's treatment. (defcustom isa-not-undoable-commands-regexp (proof-ids-to-regexp '("undo" "back")) "Regular expression matching commands which are *not* undoable." :type 'regexp :group 'isabelle-config) ;; This next function is the important one for undo operations. (defun isa-count-undos (span) "Count number of undos in a span, return the command needed to undo that far." (let ((case-fold-search nil) (ct 0) str i) (if (and span (prev-span span 'type) (not (eq (span-property (prev-span span 'type) 'type) 'comment)) (isa-goal-command-p (span-property (prev-span span 'type) 'cmd))) (concat "choplev 0" proof-terminal-string) (while span (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'vanilla) (or (proof-string-match isa-not-undoable-commands-regexp str) (setq ct (+ 1 ct)))) ((eq (span-property span 'type) 'pbp) ;; this case probably redundant for Isabelle, unless ;; we think of some nice ways of matching non-undoable ;; commands. (cond ((not (proof-string-match isa-not-undoable-commands-regexp str)) (setq i 0) (while (< i (length str)) (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct))) (setq i (+ 1 i)))) (t nil)))) (setq span (next-span span 'type))) (concat "ProofGeneral.repeat_undo " (int-to-string ct) proof-terminal-string)))) (defun isa-goal-command-p (str) "Decide whether argument is a goal or not" (proof-string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el ;; Isabelle has no concept of a Linear context, so forgetting back ;; to the declaration of a particular something makes no real ;; sense. Perhaps in the future there will be functions to remove ;; theorems from theories, but even then all we could do is ;; forget particular theorems one by one. So we ought to search ;; backwards in isa-find-and-forget, rather than forwards as ;; the old code below does. ;; MMW: this version even does nothing at all (defun isa-find-and-forget (span) proof-no-command) ;(defun isa-find-and-forget (span) ; "Return a command to be used to forget SPAN." ; (save-excursion ; ;; FIXME: bug here: too much gets retracted. ; ;; See if we are going to part way through a completely processed ; ;; buffer, in which case it should be removed from ; ;; proof-included-files-list along with any other buffers ; ;; depending on it. However, even though we send the retraction ; ;; command to Isabelle we don't want to *completely* unlock ; ;; the current buffer. How can this be avoided? ; (goto-char (point-max)) ; (skip-chars-backward " \t\n") ; (if (>= (proof-unprocessed-begin) (point)) ; (format isa-retract-thy-file-command ; (file-name-sans-extension ; (file-name-nondirectory ; (buffer-file-name)))) ; proof-no-command))) ;; BEGIN Old code (taken from Coq.el) ;(defconst isa-keywords-decl-defn-regexp ; (ids-to-regexp (append isa-keywords-decl isa-keywords-defn)) ; "Declaration and definition regexp.") ;(defun isa-find-and-forget (span) ; (let (str ans) ; (while (and span (not ans)) ; (setq str (span-property span 'cmd)) ; (cond ; ((eq (span-property span 'type) 'comment)) ; ((eq (span-property span 'type) 'goalsave) ; (setq ans (concat isa-forget-id-command ; (span-property span 'name) proof-terminal-string))) ; ((proof-string-match (concat "\\`\\(" isa-keywords-decl-defn-regexp ; "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) ; (setq ans (concat isa-forget-id-command ; (match-string 2 str) proof-terminal-string))) ; ;; If it's not a goal but it contains "Definition" then it's a ; ;; declaration ; ((and (not (isa-goal-command-p str)) ; (proof-string-match ; (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str)) ; (setq ans (concat isa-forget-id-command ; (match-string 2 str) proof-terminal-string)))) ; (setq span (next-span span 'type))) ; (or ans "COMMENT"))) ; END old code (defvar isa-current-goal 1 "Last goal that emacs looked at.") ;; Parse proofstate output. Isabelle does not display ;; named hypotheses in the proofstate output: they ;; appear as a list in each subgoal. Ignore ;; that aspect for now and just return the ;; subgoal number. (defun isa-goal-hyp () (if (looking-at proof-shell-goal-regexp) (cons 'goal (match-string 1)))) (defun isa-state-preserving-p (cmd) "Non-nil if command preserves the proofstate." (not (proof-string-match isa-not-undoable-commands-regexp cmd))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Indentation ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Sadly this is pretty pointless for Isabelle. ;; Proof scripts in Isabelle don't really have an easily-observed ;; block structure -- a case split can be done by any obscure tactic, ;; and then solved in a number of steps that bears no relation to the ;; number of cases! And the end is certainly not marked in anyway. ;; (defun isa-stack-to-indent (stack) (cond ((null stack) 0) ((null (car (car stack))) (nth 1 (car stack))) (t (save-excursion (goto-char (nth 1 (car stack))) (+ isabelle-indent (current-column)))))) (defun isa-parse-indent (c stack) "Indentation function for Isabelle. Does nothing." stack) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Isa shell startup and exit hooks ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun isa-pre-shell-start () (setq proof-prog-name isabelle-prog-name) (setq proof-mode-for-shell 'isa-shell-mode) (setq proof-mode-for-pbp 'isa-pbp-mode) (setq proof-mode-for-response 'isa-response-mode)) (defun isa-mode-config () (isa-mode-config-set-variables) (isa-init-syntax-table) (setq font-lock-keywords isa-font-lock-keywords-1) (proof-config-done) ;; outline ;; FIXME: do we need to call make-local-variable here? (make-local-variable 'outline-regexp) (setq outline-regexp isa-outline-regexp) (make-local-variable 'outline-heading-end-regexp) (setq outline-heading-end-regexp isa-outline-heading-end-regexp) ;; tags ; (and (boundp 'tag-table-alist) ; (setq tag-table-alist ; (append '(("\\.ML$" . isa-ML-file-tags-table) ; ("\\.thy$" . thy-file-tags-table)) ; tag-table-alist))) (setq blink-matching-paren-dont-ignore-comments t)) ;; This hook is added on load because proof shells can ;; be started from .thy (not in scripting mode) or .ML files. (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t) (defun isa-shell-mode-config () "Configure Proof General proof shell for Isabelle." (isa-init-output-syntax-table) (setq font-lock-keywords isa-output-font-lock-keywords-1) (isa-shell-mode-config-set-variables) (proof-shell-config-done)) (defun isa-response-mode-config () (setq font-lock-keywords isa-output-font-lock-keywords-1) (isa-init-output-syntax-table) (proof-response-config-done)) (defun isa-pbp-mode-config () ;; FIXME: next two broken, of course, as is all PBP everywhere. (setq pbp-change-goal "Show %s.") (setq pbp-error-regexp proof-shell-error-regexp) (isa-init-output-syntax-table) (setq font-lock-keywords isa-output-font-lock-keywords-1) (proof-goals-config-done)) ;; ================================================================= ;; ;; x-symbol support for Isabelle PG, provided by David von Oheimb. ;; ;; The following settings configure the generic PG package. ;; The token language "Isabelle Symbols" is in file x-symbol-isa.el ;; (setq proof-xsym-extra-modes '(isasym-mode ; FIXME: necessary? thy-mode ; FIXME: necessary? shell-mode) ; FIXME: necessary? proof-xsym-font-lock-keywords '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))) proof-xsym-activate-command "print_mode := (!print_mode union [\"xsymbols\",\"symbols\"])" proof-xsym-deactivate-command "print_mode := filter_out (fn x=>(rev (explode \"symbols\") prefix rev (explode x))) (!print_mode)") (provide 'isa)