diff options
Diffstat (limited to 'isa/isa.el')
| -rw-r--r-- | isa/isa.el | 765 |
1 files changed, 765 insertions, 0 deletions
diff --git a/isa/isa.el b/isa/isa.el new file mode 100644 index 00000000..245c17d0 --- /dev/null +++ b/isa/isa.el @@ -0,0 +1,765 @@ +;; isa-mode.el Emacs support for Isabelle proof assistant +;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Contact: isa@proofgeneral.org +;; +;; $Id$ +;; +;; ----------------------------------------------------------------- +;; +;; This file and the rest of Isabelle Proof General contain code taken +;; from David Aspinall's Isamode system, a personal project undertaken +;; 1993-1999 as a contribution to the Isabelle community. +;; +;; ----------------------------------------------------------------- + + +;; Add Isabelle image onto splash screen +;; +;; (don't use customize-set-variable since it will be saved with options!) +(setq proof-splash-extensions + '(list + nil + (proof-splash-display-image "isabelle_transparent" t))) + +;; In case Isa mode was invoked directly or by -*- isa -*- at +;; the start of the file, ensure that Isa mode is used from now +;; on for .thy and .ML files. +;; FIXME: be less messy with auto-mode-alist here (remove dups) +(setq auto-mode-alist + (cons '("\\.ML$\\|\\.thy$" . isa-mode) auto-mode-alist)) + +(require 'proof) +(require 'isa-syntax) +(require 'isabelle-system) + +;;; +;;; ======== 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) + + +;;; +;;; ======== Configuration of generic modes ======== +;;; + +(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) + +(defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.") +(defvar isa-shell-outline-heading-end-regexp "$") + + + + +(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-enclose-offset (- proof-indent) + proof-indent-open-offset 0 + proof-indent-close-offset 0 + proof-indent-any-regexp isa-indent-any-regexp + proof-indent-inner-regexp isa-indent-inner-regexp + proof-indent-enclose-regexp isa-indent-enclose-regexp + proof-indent-open-regexp isa-indent-open-regexp + proof-indent-close-regexp isa-indent-close-regexp + + ;; 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 (space_explode \",\" \"%s\");" + proof-shell-start-silent-cmd "Goals.disable_pr();" + proof-shell-stop-silent-cmd "Goals.enable_pr();" + ;; 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-state-preserving-p 'isa-state-preserving-p + + ;; 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\";" + + ;; Parsing error messages. Bit tricky to allow for + ;; multitude of possible error formats Isabelle spits out. + ;; Ideally we shouldn't bother parsing errors that appear + ;; in the temporary ML files generated while reading + ;; theories, but unfortunately the user sometimes needs to + ;; examine them to understand a strange problem... + proof-shell-next-error-regexp + "\\(error on \\|Error: in '[^']+', \\)line \\([0-9]+\\)\\|The error(s) above occurred" + proof-shell-next-error-filename-regexp + "\\(Loading theory \"\\|Error: in '\\)\\([^\"']+\\)[\"']" + proof-shell-next-error-extract-filename + "%s.thy")) + + + +(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" + + ;; This pattern is just for comint + proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?" + + ;; for issuing command, not used to track cwd in any way. + proof-shell-cd-cmd "ThyLoad.add_path \"%s\";" + + ;; Escapes for filenames inside ML strings. + ;; We also make a hack for Isabelle, by switching from backslashes + ;; to forward slashes if it looks like we're running on Windows. + proof-shell-filename-escapes + (if (fboundp 'win32-long-file-name) ; rough test for XEmacs on win32 + ;; Patterns to unixfy names. Avoids a deliberate bomb in Isabelle which + ;; barfs at paths with these characters in them. + '(("\\\\" . "/") ("\"" . "\\\"") ("^[a-zA-Z]:" . "")) + ;; Normal case: quotation for backslash, quote mark. + '(("\\\\" . "\\\\") ("\"" . "\\\""))) + + 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: not used yet. In future will be used for + ;; proof-by-pointing like features. + ;; 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 "^No subgoals!" + + ;; initial command configures Isabelle by hacking print functions, + ;; restoring settings saved by Proof General, etc. + + ;; FIXME: temporary hack for almost enabling/disabling printing. + ;; Also for setting default values. + proof-shell-pre-sync-init-cmd "ProofGeneral.init false;" + proof-shell-init-cmd (proof-assistant-settings-cmd) + + proof-shell-restart-cmd "ProofGeneral.isa_restart();" + proof-shell-quit-cmd "quit();" + + ;; NB: the settings below will only recognize tracing output in + ;; Isabelle 2001. + proof-shell-eager-annotation-start "\360\\|\362" + proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-end "\361\\|\363" + ;; see isa-pre-shell-start for proof-shell-trace-output-regexp + + ;; 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." + proof-shell-set-elisp-variable-regexp "Proof General, please set the variable \\([^ ]+\\) to: #\\([^#]+\\)#\\." + proof-shell-theorem-dependency-list-regexp "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"" + + ;; 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 + + ;; === 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))) + ;; 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 +;;; + +;; 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. + +; attempt to trap C-g. Needs more work so revert to previous +;(defun isa-update-thy-only (file try wait) +; "Tell Isabelle to update current buffer's theory, and all ancestors." +; ;; Trap interrupts from C-g during the update +; (condition-case err +; (proof-shell-invisible-command +; (format "ProofGeneral.%supdate_thy_only \"%s\";" +; (if try "try_" "") (file-name-sans-extension file)) +; wait) +; (t (message "Isabelle Proof General: error or interrupt during update theory...") +; (if proof-shell-busy +; (proof-interrupt-process)) +; (sit-for 1) +; (proof-deactivate-scripting) +; (if (cdr err) ;; quit is just (quit). +; (error (cdr err)))))) + +(defun isa-update-thy-only (file try wait) + "Tell Isabelle to update current buffer's theory, and all ancestors." + ;; First make sure we're in the right directory to take care of + ;; relative "files" paths inside theory file. + (proof-cd-sync) + (proof-shell-invisible-command + (proof-format-filename + ;; %r parameter means relative (don't expand) path + (format "ProofGeneral.%supdate_thy_only \"%%r\";" (if try "try_" "")) + (file-name-nondirectory (file-name-sans-extension file))) + wait)) + +(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 falsely leaves 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-goals-mode proof-goals-mode + "Isabelle goals" nil + (isa-goals-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))) + + +;; +;; 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) + (proof-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) + ;; 3.3 fix: add require proof-script since context menus are + ;; now added for response/goals buffer, which requires proof mode. + (unless proof-terminal-char + (require 'proof-script) + (proof-menu-define-specific) + (isa-mode-config-set-variables)) + + (thy-mode) + + ;; related mode configuration including locking buffer, + ;; fontification, etc. + (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) +(proof-define-keys map proof-universal-keys))) + +;; 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 \"%r\";" + "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." + (interactive (list buffer-file-name)) + (proof-deactivate-scripting) + (proof-shell-invisible-command + (proof-format-filename 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 +;; + +(defcustom isa-not-undoable-commands-regexp + (proof-ids-to-regexp '("undo")) + "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 cmds. + (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 code from the type theory provers does. + +;; MMW: this version even does nothing at all +(defun isa-find-and-forget (span) + proof-no-command) + +(defun isa-state-preserving-p (cmd) + "Non-nil if command preserves the proofstate." + (not (proof-string-match isa-not-undoable-commands-regexp cmd))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Isa shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun isa-pre-shell-start () + (setq proof-prog-name (isabelle-command-line)) + (setq proof-mode-for-shell 'isa-shell-mode) + (setq proof-mode-for-goals 'isa-goals-mode) + (setq proof-mode-for-response 'isa-response-mode) + (setq proof-shell-trace-output-regexp "\375")) + +(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)) + + +;; These hooks are 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) +(add-hook 'proof-shell-insert-hook 'isa-preprocessing) + +(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-goals-mode-config () + ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO. + (setq pbp-change-goal "Show %s.") + (setq pbp-error-regexp proof-shell-error-regexp) + (isa-init-output-syntax-table) + (setq font-lock-keywords isa-goals-font-lock-keywords) + (proof-goals-config-done)) + +(defun isa-preprocessing () ;dynamic scoping of `string' + "Handle ^VERBATIM marker -- acts on variable STRING by dynamic scoping" + (if (proof-string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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 '(thy-mode) + proof-xsym-activate-command + "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);" + proof-xsym-deactivate-command + "print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]);") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Completion table for Isabelle identifiers +;; +;; Ideally this could be set automatically from the running process, +;; and maybe a default value could be dumped by Isabelle when it is +;; built. + +(defpgdefault completion-table + '("quit" + "cd" "use" "use_thy" "time_use" "time_use_thy" + "Pretty.setdepth" "Pretty.setmargin" "print_depth" + "show_hyps" "show_types" "show_sorts" + "print_exn" + "goal" "goalw" "goalw_cterm" "premises" + "by" "byev" + "result" "uresult" + "chop" "choplev" "back" "undo" + "pr" "prlev" "goals_limit" + "proof_timing" + "prove_goal" "prove_goalw" "prove_goalw_cterm" + "push_proof" "pop_proof" "rotate_proof" + "save_proof" "restore_proof" + "read" "prin" "printyp" + "topthm" "getgoal" "gethyps" + "filter_goal" "compat_goal" + + ;; short cuts - should these be included? + "ba" "br" "be" "bd" "brs" "bes" "bds" + "fs" "fr" "fe" "fd" "frs" "fes" "fds" + "bw" "bws" "ren" + + "resolve_tac" "eresolve_tac" "dresolve_tac" "forward_tac" + "assume_tac" "eq_assume_tac" + "match_tac" "ematch_tac" "dmatch_tac" + "res_inst_tac" "eres_inst_tac" "dres_inst_tac" "forw_inst_tac" + "rewrite_goals_tac" "rewrite_tac" "fold_goals_tac" + "fold_goals_tac" "fold_tac" + "cut_facts_tac" "subgoal_tac" + + ;; short cuts - should these be included? + "rtac" "etac" "dtac" "atac" "ares_tac" "rewtac" + + ;; In general, I think rules should appear in rule tables, not here. + "asm_rl" "cut_rl" + + "flexflex_tac" "rename_tac" "rename_last_tac" + "Logic.set_rename_prefix" "Logic.auto_rename" + + "compose_tac" + + "biresolve_tac" "bimatch_tac" "subgoals_of_brl" "lessb" + "head_string" "insert_thm" "delete_thm" "compat_resolve_tac" + + "could_unify" "filter_thms" "filt_resolve_tac" + + ;; probably shouldn't be included: + "tapply" "Tactic" "PRIMITIVE" "STATE" "SUBGOAL" + + "pause_tac" "print_tac" + + "THEN" "ORELSE" "APPEND" "INTLEAVE" + "EVERY" "FIRST" "TRY" "REPEAT_DETERM" "REPEAT" "REPEAT1" + "trace_REPEAT" + "all_tac" "no_tac" + "FILTER" "CHANGED" "DEPTH_FIRST" "DEPTH_SOLVE" + "DEPTH_SOLVE_1" "trace_DEPTH_FIRST" + "BREADTH_FIRST" "BEST_FIRST" "THEN_BEST_FIRST" + "trace_BEST_FIRST" + "COND" "IF_UNSOLVED" "DETERM" + + "SELECT_GOAL" "METAHYPS" + + "ALLGOALS" "TRYALL" "SOMEGOAL" "FIRSTGOAL" + "REPEAT_SOME" "REPEAT_FIRST" "trace_goalno_tac" + + ;; include primed versions of tacticals? + + "EVERY1" "FIRST1" + + "prth" "prths" "prthq" + "RSN" "RLN" "RL" + + ;; simplifier + + "addsimps" "addeqcongs" "delsimps" + "setsolver" "setloop" "setmksimps" "setsubgoaler" + "empty_ss" "merge_ss" "prems_of_ss" "rep_ss" + "simp_tac" "asm_full_simp_tac" "asm_simp_tac" + + ;; classical prover + + "empty_cs" + "addDs" "addEs" "addIs" "addSDs" "addSEs" "addSIs" + "print_cs" + "rep_claset" "best_tac" "chain_tac" "contr_tac" "eq_mp_tac" + "fast_tac" "joinrules" "mp_tac" "safe_tac" "safe_step_tac" + "slow_best_tac" "slow_tac" "step_tac" "swapify" + "swap_res_tac" "inst_step_tac" + + ;; that's it for now! + )) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Theorem dependencies (experimental) +;; + +(defpacustom theorem-dependencies nil + "Whether to track theorem dependencies within Proof General." + :type 'boolean + ;; when this is built-in (or with a ":=%b" setting). + ;; :setting ("depends_enable()" . "depends_disable()") + :eval (isa-theorem-dependencies-switch)) + +(defvar isa-dependsml-file-loaded nil) + +(add-hook 'proof-shell-kill-function-hooks + (lambda () (setq isa-dependsml-file-loaded nil))) + +(defun isa-load-dependsml-file () + ;; NB: maybe doesn't work if enabled before Isabelle starts. + (if (proof-shell-available-p) + (progn + (proof-shell-invisible-command + (proof-format-filename + "use \"%r\";" + (concat (file-name-directory + (locate-library "isa")) + "depends.ML"))) + (setq isa-dependsml-file-loaded t)))) + +(defun isa-theorem-dependencies-switch () + "Switch on/off theorem dependency tracking. (Experimental feature)." + (if (and isa-theorem-dependencies (not isa-dependsml-file-loaded)) + (isa-load-dependsml-file)) + (proof-shell-invisible-command (if isa-theorem-dependencies + "depends_enable()" + "depends_disable()"))) + + + + + +(provide 'isa) |