;; isa.el Major mode for Isabelle proof assistant ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; ;; Author: David Aspinall ;; Maintainer: Isabelle maintainer ;; ;; $Id$ ;; (require 'isa-syntax) (require 'outline) (require 'proof) ;;; ;;; ======== User settings for Isabelle ======== ;;; (defgroup isabelle-settings nil "Customization of Isabelle specifics for Proof General." :group 'proof-general) (defcustom isa-prog-name "/usr/lib/Isabelle98/bin/isabelle" "*Name of program to run Isabelle." :type 'file :group 'isabelle-settings) (defcustom isa-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-settings) (defcustom isa-www-home-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-settings) ;;; ;;; ======== Configuration of generic modes ======== ;;; ;;; 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 mode variables for Isabelle." (setq proof-assistant "Isabelle" proof-www-home-page isa-www-home-page ;; proof script syntax proof-terminal-char ?\; ; ends a proof proof-comment-start "(*" ; comment in a proof proof-comment-end "*)" ; ;; proof engine output syntax proof-save-command-regexp isa-save-command-regexp proof-save-with-hole-regexp isa-save-with-hole-regexp proof-goal-with-hole-regexp isa-goal-with-hole-regexp proof-commands-regexp (ids-to-regexp isa-keywords) ;; proof engine commands (first three for menus, last for undo) proof-prf-string "pr();" proof-goal-command "Goal \"%s\";" proof-save-command "qed \"%s\";" proof-ctxt-string "ProofGeneral.show_context();" proof-help-string "ProofGeneral.help();" proof-kill-goal-command "ProofGeneral.kill_goal();" ;; 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-global-p 'isa-global-p ; FIXME: proof.el should allow nil proof-parse-indent 'isa-parse-indent proof-stack-to-indent 'isa-stack-to-indent)) (defun isa-shell-mode-config-set-variables "Configure generic proof shell mode variables for Isabelle." (setq proof-shell-prompt-pattern "^\\(val it = () : unit\n\\)?2?[-=#>]>? *" ;"^[-=#>]>? *" ;; This pattern matches a variety of prompts from ML. ;; It doesn't match the tracing output prompt. ;; Probably it isn't general enough for all MLs, please send me ;; problem reports / patches. ;; Alternative version to match vacuous assignments: ;; this doesn't work as intended, probably because the ;; process mungling searches backwards and forwards for ;; regexps. proof-shell-cd "cd \"%s\";" ;; this one not set: proof-shell-abort-goal-regexp proof-shell-proof-completed-regexp "No subgoals!" proof-shell-error-regexp isa-error-regexp proof-shell-interrupt-regexp "Interrupt" ; FIXME: only good for NJ/SML proof-shell-noise-regexp "" proof-shell-assumption-regexp isa-id ; matches name of assumptions proof-shell-goal-regexp isa-goal-regexp ; matches subgoal heading ;; We can't hack the SML prompt, so set wakeup-char to nil. proof-shell-wakeup-char nil proof-shell-start-goals-regexp "\370" proof-shell-end-goals-regexp "\371" ;; initial command configures Isabelle by hacking print functions. ;; may need to set directory somewhere for this: ;; /home/da/devel/lego/elisp/ or $PROOFGENERIC_HOME ? proof-shell-init-cmd (concat "use \"" proof-home "isa/ProofGeneral.ML\";") proof-shell-eager-annotation-start "^\\[opening " ;; proof-shell-eager-annotation-end "$" proof-shell-eager-annotation-end "$" ;; === ANNOTATIONS === ones below here are broken proof-shell-goal-char ?\375 proof-shell-first-special-char ?\360 proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern 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)) ;; ===== outline mode ;;; FIXME: test and add more things here (defvar isa-outline-regexp (ids-to-regexp '("goal" "Goal" "prove_goal")) "Outline regexp for Isabelle ML files") ;;; End of a command needs parsing to find, so this is approximate. (defvar isa-outline-heading-end-regexp ";[ \t\n]*") (defconst isa-goal-regexp "^[ \t]*[0-9]+\\. " "Regexp to match subgoal headings. Used by proof mode to parse proofstate output, and also to set outline heading regexp.") ;; (defvar isa-shell-outline-regexp isa-goal-regexp) (defvar isa-shell-outline-heading-end-regexp isa-goal-regexp) ;;; ---- end-outline ;; ;; Define the derived modes ;; (define-derived-mode isa-shell-mode proof-shell-mode "Isabelle shell" nil (isa-shell-mode-config)) (define-derived-mode isa-pbp-mode pbp-mode "Isabelle proofstate" nil (isa-pbp-mode-config)) (define-derived-mode isa-proofscript-mode proof-mode "Isabelle script" nil (isa-mode-config)) ;; Automatically selecting theory mode or Proof General script mode. (defun isa-mode () "Mode for Isabelle buffers: either isa-proofscript-mode or isa-thy-mode. Files with extension .thy will be in isa-thy-mode, otherwise we choose isa-proofscript-mode." (interactive) (cond ((string-match ".thy" (buffer-file-name)) (isa-thy-mode)) (t (isa-proofscript-mode)))) ;; Next portion taken from isa-load.el ;; isa-load.el,v 3.8 1998/09/01 (defcustom isa-use-sml-mode (if (fboundp 'sml-mode) 'sml-mode) "*If non-nil, attempt to use sml-mode in ML section of theory files." :type 'boolean :group 'isabelle-settings) (defgroup isa-thy-mode nil "Customization of Isamode's theory editing mode" ;; :link '(info-link "(Isamode)Theory Files") :load 'isa-thy-mode :group 'isabelle-settings) (autoload 'isa-thy-mode "isa-thy-mode" "Major mode for Isabelle theory files" t nil) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Code that's Isabelle specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; FIXME: think about the next variable. I've changed sense from ;; LEGO and Coq's treatment. (defconst isa-not-undoable-commands-regexp (ids-to-regexp '("undo" "back")) "Regular expression matching commands which are *not* undoable.") ;; 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 ((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 (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 (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 "choplev " (int-to-string ct) proof-terminal-string)))) (defun isa-goal-command-p (str) "Decide whether argument is a goal or not" (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. (defun isa-find-and-forget (span) ;; Special return value to indicate nothing needs to be done. 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))) ; ((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)) ; (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." (string-match isa-not-undoable-commands-regexp cmd)) ;; FIXME: I don't really know what this means, but lego sets ;; it to always return nil. Probably should be able to ;; leave it unset. (defun isa-global-p (cmd) nil) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; 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))) (+ isa-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 isa-prog-name) (setq proof-mode-for-shell 'isa-shell-mode) (setq proof-mode-for-pbp 'isa-pbp-mode)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof and pbp mode and setting up various utilities ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun isa-init-syntax-table () "Set appropriate values for syntax table in current buffer." (modify-syntax-entry ?\$ ".") (modify-syntax-entry ?\/ ".") (modify-syntax-entry ?\\ ".") (modify-syntax-entry ?+ ".") (modify-syntax-entry ?- ".") (modify-syntax-entry ?= ".") (modify-syntax-entry ?% ".") (modify-syntax-entry ?< ".") (modify-syntax-entry ?> ".") (modify-syntax-entry ?\& ".") (modify-syntax-entry ?_ "_") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") (modify-syntax-entry ?\* ". 23") (modify-syntax-entry ?\( "()1") (modify-syntax-entry ?\) ")(4")) (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$" . isa-thy-file-tags-table)) ; tag-table-alist))) (setq blink-matching-paren-dont-ignore-comments t) ;; hooks and callbacks (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t)) (defun isa-shell-mode-config () ;; The following hook is removed once it's called. ;; FIXME: maybe add this back later. ;;(add-hook 'proof-shell-insert-hook 'isa-shell-init-hook nil t) (isa-init-syntax-table) (isa-shell-mode-config-set-variables) (proof-shell-config-done)) ;; FIXME: broken, of course, as is all PBP everywhere. (defun isa-pbp-mode-config () (setq pbp-change-goal "Show %s.") (setq pbp-error-regexp isa-error-regexp)) (provide 'isa)