| 1 | ; isar.el Major mode for Isabelle/Isar proof assistant |
|---|
| 2 | ;; Copyright (C) 1994-2004 LFCS Edinburgh. |
|---|
| 3 | ;; |
|---|
| 4 | ;; License: GPL (GNU GENERAL PUBLIC LICENSE) |
|---|
| 5 | ;; |
|---|
| 6 | ;; Maintainers: David Aspinall, Stefan Berghofer |
|---|
| 7 | ;; |
|---|
| 8 | ;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> |
|---|
| 9 | ;; Markus Wenzel <wenzelm@in.tum.de> |
|---|
| 10 | ;; |
|---|
| 11 | ;; Contributors: David von Oheimb, Sebastian Skalberg |
|---|
| 12 | ;; |
|---|
| 13 | ;; |
|---|
| 14 | ;; $Id: isar.el,v 8.29 2007/03/03 15:28:20 da Exp $ |
|---|
| 15 | ;; |
|---|
| 16 | |
|---|
| 17 | (require 'proof) |
|---|
| 18 | |
|---|
| 19 | ;; "Find Theorems" search form |
|---|
| 20 | (require 'find-theorems) |
|---|
| 21 | |
|---|
| 22 | ;; System code |
|---|
| 23 | (require 'isabelle-system) |
|---|
| 24 | |
|---|
| 25 | ;; |
|---|
| 26 | ;; Load syntax |
|---|
| 27 | ;; |
|---|
| 28 | (defcustom isar-keywords-name nil |
|---|
| 29 | "Specifies a theory-specific keywords setting to use with Isar. |
|---|
| 30 | See -k option for Isabelle interface script." |
|---|
| 31 | :type 'string |
|---|
| 32 | :group 'isabelle-isar) |
|---|
| 33 | |
|---|
| 34 | (or (featurep 'isar-keywords) |
|---|
| 35 | ;; Pickup isar-keywords file from somewhere appropriate, |
|---|
| 36 | ;; giving user chance to set name of file, or based on |
|---|
| 37 | ;; name of logic. |
|---|
| 38 | (isabelle-load-isar-keywords |
|---|
| 39 | (or isar-keywords-name |
|---|
| 40 | isabelle-chosen-logic))) |
|---|
| 41 | (require 'isar-syntax) |
|---|
| 42 | |
|---|
| 43 | |
|---|
| 44 | ;; Completion table for Isabelle/Isar identifiers |
|---|
| 45 | (defpgdefault completion-table isar-keywords-major) |
|---|
| 46 | |
|---|
| 47 | (defcustom isar-web-page |
|---|
| 48 | "http://isabelle.in.tum.de/Isar/" |
|---|
| 49 | "URL of web page for Isabelle/Isar." |
|---|
| 50 | :type 'string |
|---|
| 51 | :group 'isabelle-isar) |
|---|
| 52 | |
|---|
| 53 | |
|---|
| 54 | ;; Adjust toolbar entries (must be done before proof-toolbar is loaded). |
|---|
| 55 | |
|---|
| 56 | (if proof-running-on-XEmacs |
|---|
| 57 | (setq isar-toolbar-entries |
|---|
| 58 | (remassoc 'qed (remassoc 'goal isar-toolbar-entries)))) |
|---|
| 59 | |
|---|
| 60 | |
|---|
| 61 | (defun isar-strip-terminators () |
|---|
| 62 | "Remove explicit Isabelle/Isar command terminators `;' from the buffer." |
|---|
| 63 | (interactive) |
|---|
| 64 | (save-excursion |
|---|
| 65 | (goto-char (point-min)) |
|---|
| 66 | (while (proof-search-forward ";" (point-max) t) |
|---|
| 67 | (if (not (proof-buffer-syntactic-context)) |
|---|
| 68 | (progn |
|---|
| 69 | (delete-backward-char 1) |
|---|
| 70 | (or (proof-looking-at ";\\|\\s-\\|$") |
|---|
| 71 | (insert " "))))))) |
|---|
| 72 | |
|---|
| 73 | |
|---|
| 74 | (defun isar-markup-ml (string) |
|---|
| 75 | "Return marked up version of ML command STRING for Isar." |
|---|
| 76 | (format "ML_command {* %s *};" string)) |
|---|
| 77 | |
|---|
| 78 | |
|---|
| 79 | (defun isar-mode-config-set-variables () |
|---|
| 80 | "Configure generic proof scripting mode variables for Isabelle/Isar." |
|---|
| 81 | (setq |
|---|
| 82 | proof-assistant-home-page isar-web-page |
|---|
| 83 | proof-mode-for-script 'isar-mode |
|---|
| 84 | ;; proof script syntax |
|---|
| 85 | proof-terminal-char ?\; ; forcibly ends a command |
|---|
| 86 | proof-script-command-start-regexp |
|---|
| 87 | (proof-regexp-alt |
|---|
| 88 | ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *} |
|---|
| 89 | ;; because that's lexically a kind of comment. |
|---|
| 90 | isar-any-command-regexp |
|---|
| 91 | (regexp-quote ";")) |
|---|
| 92 | proof-script-integral-proofs t |
|---|
| 93 | ;; FIXME: use old parser for now to avoid { } problem |
|---|
| 94 | proof-script-use-old-parser t |
|---|
| 95 | proof-script-comment-start isar-comment-start |
|---|
| 96 | proof-script-comment-end isar-comment-end |
|---|
| 97 | proof-script-comment-start-regexp isar-comment-start-regexp |
|---|
| 98 | proof-script-comment-end-regexp isar-comment-end-regexp |
|---|
| 99 | proof-string-start-regexp isar-string-start-regexp |
|---|
| 100 | proof-string-end-regexp isar-string-end-regexp |
|---|
| 101 | |
|---|
| 102 | ;; Next few used for func-menu and recognizing goal..save regions in |
|---|
| 103 | ;; script buffer. |
|---|
| 104 | proof-save-command-regexp isar-save-command-regexp |
|---|
| 105 | proof-goal-command-regexp isar-goal-command-regexp |
|---|
| 106 | proof-goal-with-hole-regexp isar-named-entity-regexp |
|---|
| 107 | proof-goal-with-hole-result 2 |
|---|
| 108 | proof-save-with-hole-regexp nil |
|---|
| 109 | proof-script-next-entity-regexps isar-next-entity-regexps |
|---|
| 110 | proof-script-imenu-generic-expression isar-generic-expression |
|---|
| 111 | imenu-syntax-alist isar-script-syntax-table-alist |
|---|
| 112 | |
|---|
| 113 | proof-indent-enclose-offset (- proof-indent) |
|---|
| 114 | proof-indent-open-offset 0 |
|---|
| 115 | proof-indent-close-offset 0 |
|---|
| 116 | proof-indent-any-regexp isar-indent-any-regexp |
|---|
| 117 | ; proof-indent-inner-regexp isar-indent-inner-regexp |
|---|
| 118 | proof-indent-enclose-regexp isar-indent-enclose-regexp |
|---|
| 119 | proof-indent-open-regexp isar-indent-open-regexp |
|---|
| 120 | proof-indent-close-regexp isar-indent-close-regexp |
|---|
| 121 | |
|---|
| 122 | ;; proof engine commands |
|---|
| 123 | proof-showproof-command "pr" |
|---|
| 124 | proof-goal-command "lemma \"%s\"" |
|---|
| 125 | proof-save-command "qed" |
|---|
| 126 | proof-context-command "print_context" |
|---|
| 127 | proof-info-command "welcome" |
|---|
| 128 | proof-kill-goal-command "ProofGeneral.kill_proof" |
|---|
| 129 | ; proof-find-theorems-command "find_theorems %s" ;; minibuffer |
|---|
| 130 | ; proof-find-theorems-command 'proof-find-theorems-minibuffer ;; equivalent |
|---|
| 131 | proof-find-theorems-command 'proof-find-theorems-form ;; search form |
|---|
| 132 | proof-shell-start-silent-cmd "disable_pr" |
|---|
| 133 | proof-shell-stop-silent-cmd "enable_pr" |
|---|
| 134 | ;; command hooks |
|---|
| 135 | proof-goal-command-p 'isar-goal-command-p |
|---|
| 136 | proof-really-save-command-p 'isar-global-save-command-p |
|---|
| 137 | proof-count-undos-fn 'isar-count-undos |
|---|
| 138 | proof-find-and-forget-fn 'isar-find-and-forget |
|---|
| 139 | proof-state-preserving-p 'isar-state-preserving-p |
|---|
| 140 | proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list |
|---|
| 141 | ;; span menu |
|---|
| 142 | proof-script-span-context-menu-extensions 'isabelle-create-span-menu)) |
|---|
| 143 | |
|---|
| 144 | |
|---|
| 145 | (defun isar-shell-mode-config-set-variables () |
|---|
| 146 | "Configure generic proof shell mode variables for Isabelle/Isar." |
|---|
| 147 | (setq |
|---|
| 148 | pg-subterm-first-special-char ?\350 |
|---|
| 149 | proof-shell-wakeup-char nil |
|---|
| 150 | proof-shell-annotated-prompt-regexp "^\\w*[>#] \372\\|^\\w*[>#] \^AS" |
|---|
| 151 | |
|---|
| 152 | ;; This pattern is just for comint. |
|---|
| 153 | proof-shell-prompt-pattern "^\\w*[>#] " |
|---|
| 154 | |
|---|
| 155 | ;; for issuing command, not used to track cwd in any way. |
|---|
| 156 | proof-shell-cd-cmd (isar-markup-ml "ThyLoad.add_path \"%s\"") |
|---|
| 157 | |
|---|
| 158 | ;; Escapes for filenames inside ML strings. |
|---|
| 159 | ;; We also make a hack for a bug in Isabelle, by switching from |
|---|
| 160 | ;; backslashes to forward slashes if it looks like we're running |
|---|
| 161 | ;; on Windows. |
|---|
| 162 | proof-shell-filename-escapes |
|---|
| 163 | (if (fboundp 'win32-long-filename) ; rough test for XEmacs on win32 |
|---|
| 164 | ;; Patterns to unixfy names. |
|---|
| 165 | ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "") |
|---|
| 166 | ;; But I'll risk leaving drive names in, not sure how to replace them. |
|---|
| 167 | '(("\\\\" . "/") ("\"" . "\\\"")) |
|---|
| 168 | ;; Normal case: quotation for backslash, quote mark. |
|---|
| 169 | '(("\\\\" . "\\\\") ("\"" . "\\\""))) |
|---|
| 170 | |
|---|
| 171 | proof-shell-proof-completed-regexp nil ; n.a. |
|---|
| 172 | proof-shell-interrupt-regexp "\364\\*\\*\\* Interrupt\\|\^AM\\*\\*\\* Interrupt" |
|---|
| 173 | proof-shell-error-regexp "\364\\*\\*\\*\\|\^AM\\*\\*\\*" |
|---|
| 174 | proof-shell-abort-goal-regexp nil ; n.a. |
|---|
| 175 | |
|---|
| 176 | ;; |
|---|
| 177 | pg-next-error-regexp "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)" |
|---|
| 178 | pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)" |
|---|
| 179 | |
|---|
| 180 | ;; matches names of assumptions |
|---|
| 181 | proof-shell-assumption-regexp isar-id |
|---|
| 182 | |
|---|
| 183 | proof-shell-start-goals-regexp "\366\n\\|\^AO\n" |
|---|
| 184 | proof-shell-end-goals-regexp "\367\\|\^AP" |
|---|
| 185 | |
|---|
| 186 | ;; FIXME: next one is needed for backward compatibility. |
|---|
| 187 | ;; Would be nice to remove this somehow else, it's only used for |
|---|
| 188 | ;; Isar and pre-PGIP. One way would be to hack the |
|---|
| 189 | ;; (now obsolete) defpacustom calls. |
|---|
| 190 | proof-assistant-setting-format |
|---|
| 191 | (unless isa-supports-pgip 'isar-markup-ml) |
|---|
| 192 | |
|---|
| 193 | proof-shell-init-cmd nil |
|---|
| 194 | proof-shell-restart-cmd "ProofGeneral.restart" |
|---|
| 195 | |
|---|
| 196 | proof-shell-eager-annotation-start-length 1 |
|---|
| 197 | proof-shell-eager-annotation-start "\360\\|\362\\|\^AI\\|\^AK" |
|---|
| 198 | proof-shell-eager-annotation-end "\361\\|\363\\|\^AJ\\|\^AL" |
|---|
| 199 | ;; see isar-pre-shell-start for proof-shell-trace-output-regexp |
|---|
| 200 | |
|---|
| 201 | ;; Isabelle is learning to talk PGIP... |
|---|
| 202 | proof-shell-match-pgip-cmd "<pgip" |
|---|
| 203 | proof-shell-issue-pgip-cmd |
|---|
| 204 | (if isa-supports-pgip 'isabelle-process-pgip nil) |
|---|
| 205 | |
|---|
| 206 | ;; Some messages delimited by eager annotations |
|---|
| 207 | proof-shell-clear-response-regexp "Proof General, please clear the response buffer." |
|---|
| 208 | proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." |
|---|
| 209 | |
|---|
| 210 | ;; Theorem dependencies. NB: next regex anchored at end with eager annot end |
|---|
| 211 | proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\361\\|\^AJ\\)" |
|---|
| 212 | proof-shell-theorem-dependency-list-split "\" \"" |
|---|
| 213 | proof-shell-show-dependency-cmd "thm %s;" |
|---|
| 214 | proof-shell-identifier-under-mouse-cmd |
|---|
| 215 | '((nil "thm %s;") |
|---|
| 216 | (string "term \"%s\";") |
|---|
| 217 | (comment "term \"%s\";")) |
|---|
| 218 | |
|---|
| 219 | ;; Allow font-locking for output based on hidden annotations, see |
|---|
| 220 | ;; isar-output-font-lock-keywords-1 |
|---|
| 221 | pg-use-specials-for-fontify t |
|---|
| 222 | pg-special-char-regexp ;; should be: "[\200-\377]\\|\^A[A-Z]" |
|---|
| 223 | ;; da: the character range here fails to match (actually, fails |
|---|
| 224 | ;; to match-replace) in xemacs 21.5 betas, so I'm listing the |
|---|
| 225 | ;; characters instead, which works. |
|---|
| 226 | ;; This should probably be tuned to the ones actually used by Isabelle |
|---|
| 227 | "\\|\\|\\|\\|\\|
\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\|\\| \\|¡\\|¢\\|£\\|€\\|¥\\|Š\\|§\\|š\\|©\\|ª\\|«\\|¬\\|\\|®\\|¯\\|°\\|±\\|²\\|³\\|Ž\\|µ\\|¶\\|·\\|ž\\|¹\\|º\\|»\\|Œ\\|œ\\|Ÿ\\|¿\\|À\\|Á\\|Â\\|Ã\\|Ä\\|Å\\|Æ\\|Ç\\|È\\|É\\|Ê\\|Ë\\|Ì\\|Í\\|Î\\|Ï\\|Ð\\|Ñ\\|Ò\\|Ó\\|Ô\\|Õ\\|Ö\\|×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|à\\|á\\|â\\|ã\\|ä\\|å\\|æ\\|ç\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|[A-Z]" |
|---|
| 228 | pg-after-fontify-output-hook 'pg-remove-specials |
|---|
| 229 | pg-subterm-help-cmd "term %s" |
|---|
| 230 | |
|---|
| 231 | proof-cannot-reopen-processed-files t |
|---|
| 232 | proof-shell-process-file |
|---|
| 233 | (cons |
|---|
| 234 | ;; Theory loader output |
|---|
| 235 | "Proof General, this file is loaded: \"\\(.*\\)\"" |
|---|
| 236 | (lambda (str) |
|---|
| 237 | (match-string 1 str))) |
|---|
| 238 | proof-shell-retract-files-regexp |
|---|
| 239 | "Proof General, you can unlock the file \"\\(.*\\)\"" |
|---|
| 240 | proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list |
|---|
| 241 | proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\"" |
|---|
| 242 | proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\"") |
|---|
| 243 | (add-hook 'proof-activate-scripting-hook 'isar-activate-scripting)) |
|---|
| 244 | |
|---|
| 245 | |
|---|
| 246 | ;;; |
|---|
| 247 | ;;; Theory loader operations |
|---|
| 248 | ;;; |
|---|
| 249 | |
|---|
| 250 | (defun isar-remove-file (name files cmp-base) |
|---|
| 251 | (if (not files) nil |
|---|
| 252 | (let* |
|---|
| 253 | ((file (car files)) |
|---|
| 254 | (rest (cdr files)) |
|---|
| 255 | (same (if cmp-base (string= name (file-name-nondirectory file)) |
|---|
| 256 | (string= name file)))) |
|---|
| 257 | (if same (isar-remove-file name rest cmp-base) |
|---|
| 258 | (cons file (isar-remove-file name rest cmp-base)))))) |
|---|
| 259 | |
|---|
| 260 | (defun isar-shell-compute-new-files-list (str) |
|---|
| 261 | "Compute the new list of files read by the proof assistant. |
|---|
| 262 | This is called when Proof General spots output matching |
|---|
| 263 | proof-shell-retract-files-regexp." |
|---|
| 264 | (let* |
|---|
| 265 | ((name (match-string 1 str)) |
|---|
| 266 | (base-name (file-name-nondirectory name))) |
|---|
| 267 | (if (string= name base-name) |
|---|
| 268 | (isar-remove-file name proof-included-files-list t) |
|---|
| 269 | (isar-remove-file (file-truename name) proof-included-files-list nil)))) |
|---|
| 270 | |
|---|
| 271 | (defun isar-activate-scripting () |
|---|
| 272 | "Make sure the Isabelle/Isar toplevel is in a sane state." |
|---|
| 273 | (proof-cd-sync)) |
|---|
| 274 | |
|---|
| 275 | |
|---|
| 276 | ;; |
|---|
| 277 | ;; Define the derived modes |
|---|
| 278 | ;; |
|---|
| 279 | (eval-and-compile |
|---|
| 280 | (define-derived-mode isar-shell-mode proof-shell-mode |
|---|
| 281 | "Isar shell" nil |
|---|
| 282 | (isar-shell-mode-config))) |
|---|
| 283 | |
|---|
| 284 | (eval-and-compile |
|---|
| 285 | (define-derived-mode isar-response-mode proof-response-mode |
|---|
| 286 | "response" nil |
|---|
| 287 | (isar-response-mode-config))) |
|---|
| 288 | |
|---|
| 289 | (eval-and-compile ; to define vars for byte comp. |
|---|
| 290 | (define-derived-mode isar-goals-mode proof-goals-mode |
|---|
| 291 | "proofstate" nil |
|---|
| 292 | (isar-goals-mode-config))) |
|---|
| 293 | |
|---|
| 294 | (eval-and-compile ; to define vars for byte comp. |
|---|
| 295 | (define-derived-mode isar-mode proof-mode |
|---|
| 296 | "Isar script" nil |
|---|
| 297 | (isar-mode-config))) |
|---|
| 298 | |
|---|
| 299 | |
|---|
| 300 | |
|---|
| 301 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 302 | ;; Code that's Isabelle/Isar specific ;; |
|---|
| 303 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 304 | |
|---|
| 305 | ;;; |
|---|
| 306 | ;;; help menu |
|---|
| 307 | ;;; |
|---|
| 308 | |
|---|
| 309 | ;;; da: how about a `C-c C-a h ?' for listing available keys? |
|---|
| 310 | |
|---|
| 311 | ;;; NB: definvisible must come after derived modes because uses |
|---|
| 312 | ;;; isar-mode-map |
|---|
| 313 | (proof-definvisible isar-help-antiquotations "print_antiquotations" [h A]) |
|---|
| 314 | (proof-definvisible isar-help-attributes "print_attributes" [h a]) |
|---|
| 315 | (proof-definvisible isar-help-cases "print_cases" [h c]) |
|---|
| 316 | (proof-definvisible isar-help-claset "print_claset" [h C]) |
|---|
| 317 | (proof-definvisible isar-help-commands "print_commands" [h o]) |
|---|
| 318 | (proof-definvisible isar-help-facts "print_facts" [h f]) |
|---|
| 319 | (proof-definvisible isar-help-syntax "print_syntax" [h i]) |
|---|
| 320 | (proof-definvisible isar-help-induct-rules "print_induct_rules" [h I]) |
|---|
| 321 | (proof-definvisible isar-help-methods "print_methods" [h m]) |
|---|
| 322 | (proof-definvisible isar-help-simpset "print_simpset" [h S]) |
|---|
| 323 | (proof-definvisible isar-help-binds "print_binds" [h b]) |
|---|
| 324 | (proof-definvisible isar-help-theorems "print_theorems" [h t]) |
|---|
| 325 | (proof-definvisible isar-help-trans-rules "print_trans_rules" [h T]) |
|---|
| 326 | |
|---|
| 327 | ;; |
|---|
| 328 | ;; Command menu |
|---|
| 329 | ;; |
|---|
| 330 | |
|---|
| 331 | ;; NB: would be nice to query save of the buffer first for these |
|---|
| 332 | ;; next two: but only convenient emacs functions offer save for |
|---|
| 333 | ;; all buffers. |
|---|
| 334 | (proof-definvisible isar-cmd-display-draft |
|---|
| 335 | '(format "display_drafts \"%s\"" buffer-file-name) |
|---|
| 336 | [(control d)]) |
|---|
| 337 | |
|---|
| 338 | (proof-definvisible isar-cmd-print-draft |
|---|
| 339 | '(if (y-or-n-p |
|---|
| 340 | (format "Print draft of file %s ?" buffer-file-name)) |
|---|
| 341 | (format "print_drafts \"%s\"" buffer-file-name) |
|---|
| 342 | (error "Aborted.")) |
|---|
| 343 | [(control p)]) |
|---|
| 344 | |
|---|
| 345 | (proof-definvisible isar-cmd-refute "refute" [?r]) |
|---|
| 346 | (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)]) |
|---|
| 347 | |
|---|
| 348 | (defpgdefault menu-entries |
|---|
| 349 | (append |
|---|
| 350 | (list isabelle-logics-menu) |
|---|
| 351 | (list |
|---|
| 352 | (cons "Commands" |
|---|
| 353 | (list |
|---|
| 354 | ["refute" isar-cmd-refute t] |
|---|
| 355 | ["quickcheck" isar-cmd-quickcheck t] |
|---|
| 356 | ["display draft" isar-cmd-display-draft t]))) |
|---|
| 357 | (list |
|---|
| 358 | (cons "Show me ..." |
|---|
| 359 | (list |
|---|
| 360 | ["cases" isar-help-cases t] |
|---|
| 361 | ["facts" isar-help-facts t] |
|---|
| 362 | ["term bindings" isar-help-binds t] |
|---|
| 363 | "----" |
|---|
| 364 | ["classical rules" isar-help-claset t] |
|---|
| 365 | ["induct/cases rules" isar-help-induct-rules t] |
|---|
| 366 | ["simplifier rules" isar-help-simpset t] |
|---|
| 367 | ["theorems" isar-help-theorems t] |
|---|
| 368 | ["transitivity rules" isar-help-trans-rules t] |
|---|
| 369 | "----" |
|---|
| 370 | ["antiquotations" isar-help-antiquotations t] |
|---|
| 371 | ["attributes" isar-help-attributes t] |
|---|
| 372 | ["commands" isar-help-commands t] |
|---|
| 373 | ["inner syntax" isar-help-syntax t] |
|---|
| 374 | ["methods" isar-help-methods t]))))) |
|---|
| 375 | |
|---|
| 376 | ;; undo proof commands |
|---|
| 377 | (defun isar-count-undos (span) |
|---|
| 378 | "Count number of undos in a span, return the command needed to undo that far." |
|---|
| 379 | (let |
|---|
| 380 | ((case-fold-search nil) ;FIXME ?? |
|---|
| 381 | (ct 0) str i) |
|---|
| 382 | (while span |
|---|
| 383 | (setq str (or (span-property span 'cmd) "")) |
|---|
| 384 | (cond ((eq (span-property span 'type) 'vanilla) |
|---|
| 385 | (or (proof-string-match isar-undo-skip-regexp str) |
|---|
| 386 | (proof-string-match isar-undo-ignore-regexp str) |
|---|
| 387 | (setq ct (+ 1 ct)))) |
|---|
| 388 | ((eq (span-property span 'type) 'pbp) ;FIXME dead code? |
|---|
| 389 | ;; this case probably redundant for Isabelle, unless |
|---|
| 390 | ;; we think of some nice ways of matching non-undoable |
|---|
| 391 | ;; commands. |
|---|
| 392 | (cond ((not (proof-string-match isar-undo-skip-regexp str)) |
|---|
| 393 | (setq i 0) |
|---|
| 394 | (while (< i (length str)) |
|---|
| 395 | (if (= (aref str i) proof-terminal-char) |
|---|
| 396 | (setq ct (+ 1 ct))) |
|---|
| 397 | (setq i (+ 1 i)))) |
|---|
| 398 | (t nil)))) |
|---|
| 399 | (setq span (next-span span 'type))) |
|---|
| 400 | (isar-undos ct))) |
|---|
| 401 | |
|---|
| 402 | ;; begin keyword |
|---|
| 403 | (defun isar-detect-begin (span) |
|---|
| 404 | "Detect the begin keyword within a command span" |
|---|
| 405 | (let ((found nil) |
|---|
| 406 | (start (span-start span)) |
|---|
| 407 | (end (span-end span))) |
|---|
| 408 | (save-excursion |
|---|
| 409 | (goto-char start) |
|---|
| 410 | (while (and (not found) (proof-search-forward isar-keyword-begin end t)) |
|---|
| 411 | (or (proof-buffer-syntactic-context) (setq found t)))) |
|---|
| 412 | found)) |
|---|
| 413 | |
|---|
| 414 | ;; command nesting |
|---|
| 415 | (defun isar-command-nested (span) |
|---|
| 416 | "Determine theory command nesting" |
|---|
| 417 | (let ((nesting 0) str) |
|---|
| 418 | (while span |
|---|
| 419 | (setq str (or (span-property span 'cmd) "")) |
|---|
| 420 | (cond |
|---|
| 421 | ;; end |
|---|
| 422 | ((proof-string-match isar-end-regexp str) |
|---|
| 423 | (decf nesting)) |
|---|
| 424 | ;; begin |
|---|
| 425 | ((or (proof-string-match isar-theory-start-regexp str) |
|---|
| 426 | (isar-detect-begin span)) |
|---|
| 427 | (incf nesting))) |
|---|
| 428 | (setq span (prev-span span 'type))) |
|---|
| 429 | (> nesting 0))) |
|---|
| 430 | |
|---|
| 431 | ;; undo theory commands |
|---|
| 432 | (defun isar-find-and-forget (span) |
|---|
| 433 | "Return commands to be used to forget SPAN." |
|---|
| 434 | (let (str ans answers) |
|---|
| 435 | (while span |
|---|
| 436 | (setq str (or (span-property span 'cmd) "")) |
|---|
| 437 | (setq ans nil) |
|---|
| 438 | (cond |
|---|
| 439 | ;; comment, diagnostic, nested proof command: skip |
|---|
| 440 | ;; (da: adding new span types may break this code, |
|---|
| 441 | ;; ought to test for type 'cmd before looking at |
|---|
| 442 | ;; str below) |
|---|
| 443 | ;; FIXME: should adjust proof-nesting-depth here. |
|---|
| 444 | ((or (eq (span-property span 'type) 'comment) |
|---|
| 445 | (eq (span-property span 'type) 'proverproc) |
|---|
| 446 | (eq (span-property span 'type) 'proof); da: needed? |
|---|
| 447 | (proof-string-match isar-undo-skip-regexp str) |
|---|
| 448 | (proof-string-match isar-undo-ignore-regexp str))) |
|---|
| 449 | ;; finished goal: undo |
|---|
| 450 | ((eq (span-property span 'type) 'goalsave) |
|---|
| 451 | (setq ans isar-undo)) |
|---|
| 452 | ;; open goal: skip and exit |
|---|
| 453 | ((proof-string-match isar-goal-command-regexp str) |
|---|
| 454 | (setq span nil)) |
|---|
| 455 | ;; nested end: undo |
|---|
| 456 | ((and (proof-string-match isar-end-regexp str) |
|---|
| 457 | (isar-command-nested span)) |
|---|
| 458 | (setq ans isar-undo)) |
|---|
| 459 | ;; not undoable: fail and exit |
|---|
| 460 | ;; [da: this is an odd case: it issues cannot_undo command to Isar, |
|---|
| 461 | ;; which immediately generates an error, I think it's a bit confusing |
|---|
| 462 | ;; for the user] |
|---|
| 463 | ((and (proof-string-match isar-undo-fail-regexp str)) |
|---|
| 464 | (setq answers nil) |
|---|
| 465 | (setq ans (isar-cannot-undo str)) |
|---|
| 466 | (setq span nil)) |
|---|
| 467 | ;; theory: remove and exit |
|---|
| 468 | ((proof-string-match isar-undo-remove-regexp str) |
|---|
| 469 | (setq ans (isar-remove (match-string 2 str))) |
|---|
| 470 | (setq span nil)) |
|---|
| 471 | ;; else: undo |
|---|
| 472 | (t |
|---|
| 473 | (setq ans isar-undo))) |
|---|
| 474 | (if ans (setq answers (cons ans answers))) |
|---|
| 475 | (if span (setq span (next-span span 'type)))) |
|---|
| 476 | (if (null answers) proof-no-command (apply 'concat answers)))) |
|---|
| 477 | |
|---|
| 478 | |
|---|
| 479 | |
|---|
| 480 | (defun isar-goal-command-p (span) |
|---|
| 481 | "Decide whether argument is a goal or not" |
|---|
| 482 | (proof-string-match isar-goal-command-regexp |
|---|
| 483 | (or (span-property span 'cmd) ""))) |
|---|
| 484 | |
|---|
| 485 | (defun isar-global-save-command-p (span str) |
|---|
| 486 | "Decide whether argument really is a global save command" |
|---|
| 487 | (or |
|---|
| 488 | (proof-string-match isar-global-save-command-regexp str) |
|---|
| 489 | (let ((ans nil) (lev 0) cmd) |
|---|
| 490 | (while (and (not ans) span (setq span (prev-span span 'type))) |
|---|
| 491 | (setq cmd (or (span-property span 'cmd) "")) |
|---|
| 492 | (cond |
|---|
| 493 | ;; comment: skip |
|---|
| 494 | ((eq (span-property span 'type) 'comment)) |
|---|
| 495 | ;; local qed: enter block |
|---|
| 496 | ((proof-string-match isar-save-command-regexp cmd) |
|---|
| 497 | (setq lev (+ lev 1))) |
|---|
| 498 | ;; local goal: leave block, or done |
|---|
| 499 | ((proof-string-match isar-local-goal-command-regexp cmd) |
|---|
| 500 | (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) |
|---|
| 501 | ;; global goal: done |
|---|
| 502 | ((proof-string-match isar-goal-command-regexp cmd) |
|---|
| 503 | (setq ans 'yes)))) |
|---|
| 504 | (eq ans 'yes)))) |
|---|
| 505 | |
|---|
| 506 | (defvar isar-current-goal 1 |
|---|
| 507 | "Last goal that emacs looked at.") |
|---|
| 508 | |
|---|
| 509 | (defun isar-state-preserving-p (cmd) |
|---|
| 510 | "Non-nil if command preserves the proofstate." |
|---|
| 511 | (proof-string-match isar-undo-skip-regexp cmd)) |
|---|
| 512 | |
|---|
| 513 | |
|---|
| 514 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 515 | ;; Commands specific to isar ;; |
|---|
| 516 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 517 | |
|---|
| 518 | (proof-defshortcut isar-bold "\\<^bold>%p" [(control b)]) |
|---|
| 519 | (proof-defshortcut isar-local "\\<^loc>%p" [(control c)]) |
|---|
| 520 | (proof-defshortcut isar-super "\\<^sup>%p" [(control u)]) |
|---|
| 521 | (proof-defshortcut isar-sub "\\<^sub>%p" [(control l)]) |
|---|
| 522 | (proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [u]) |
|---|
| 523 | (proof-defshortcut isar-longsub "\\<^bsub>%p\\<^esub>" [l]) |
|---|
| 524 | (proof-defshortcut isar-idsub "\\<^isub>%p" [(control i)]) |
|---|
| 525 | (proof-defshortcut isar-raw "\\<^raw:%p>" [(control r)]) |
|---|
| 526 | (proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)]) |
|---|
| 527 | |
|---|
| 528 | |
|---|
| 529 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 530 | ;; Isar shell startup and exit hooks ;; |
|---|
| 531 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 532 | |
|---|
| 533 | ;borrowed from plastic.el |
|---|
| 534 | (defvar isar-shell-current-line-width nil |
|---|
| 535 | "Current line width of the Isabelle process's pretty printing module. |
|---|
| 536 | Its value will be updated whenever the corresponding screen gets |
|---|
| 537 | selected.") |
|---|
| 538 | |
|---|
| 539 | ;borrowed from plastic.el |
|---|
| 540 | (defun isar-shell-adjust-line-width () |
|---|
| 541 | "Use Isabelle's pretty printing facilities to adjust output line width. |
|---|
| 542 | Checks the width in the `proof-goals-buffer'" |
|---|
| 543 | (let ((ans "")) |
|---|
| 544 | (and (buffer-live-p proof-goals-buffer) |
|---|
| 545 | (proof-shell-live-buffer) |
|---|
| 546 | (save-excursion |
|---|
| 547 | (set-buffer proof-goals-buffer) |
|---|
| 548 | (let ((current-width |
|---|
| 549 | ;; Actually, one might sometimes |
|---|
| 550 | ;; want to get the width of the proof-response-buffer |
|---|
| 551 | ;; instead. Never mind. |
|---|
| 552 | (max 20 (window-width (get-buffer-window proof-goals-buffer t))))) |
|---|
| 553 | |
|---|
| 554 | (if (equal current-width isar-shell-current-line-width) () |
|---|
| 555 | (setq isar-shell-current-line-width current-width) |
|---|
| 556 | (set-buffer proof-shell-buffer) |
|---|
| 557 | (setq ans (format "pretty_setmargin %d;" (- current-width 4))))))) |
|---|
| 558 | ans)) |
|---|
| 559 | |
|---|
| 560 | (defun isar-pre-shell-start () |
|---|
| 561 | (setq proof-prog-name (isabelle-command-line)) |
|---|
| 562 | (setq proof-mode-for-shell 'isar-shell-mode) |
|---|
| 563 | (setq proof-mode-for-goals 'isar-goals-mode) |
|---|
| 564 | (setq proof-mode-for-response 'isar-response-mode) |
|---|
| 565 | (setq proof-shell-trace-output-regexp "\375\\|\^AV")) |
|---|
| 566 | |
|---|
| 567 | |
|---|
| 568 | ;; |
|---|
| 569 | ;; Configuring proof output buffer |
|---|
| 570 | ;; |
|---|
| 571 | |
|---|
| 572 | (defun isar-preprocessing () ;dynamic scoping of `string' |
|---|
| 573 | "Insert sync markers - acts on variable STRING by dynamic scoping" |
|---|
| 574 | (if (proof-string-match isabelle-verbatim-regexp string) |
|---|
| 575 | (setq string (match-string 1 string)) |
|---|
| 576 | (unless (proof-string-match ";[ \t]*\\'" string) |
|---|
| 577 | (setq string (concat string ";"))) |
|---|
| 578 | (setq string (concat |
|---|
| 579 | "\\<^sync>" |
|---|
| 580 | (isar-shell-adjust-line-width) |
|---|
| 581 | ;; da: this was an attempted hack to deal with ML files, |
|---|
| 582 | ;; unfortunately Isar complains about not seeing a theory |
|---|
| 583 | ;; command first: ML_setup illegal at first line |
|---|
| 584 | ;; Another failure is that: (* comment *) foo; |
|---|
| 585 | ;; ignores foo. This could be fixed by scanning for |
|---|
| 586 | ;; comment end in proof-script.el's function |
|---|
| 587 | ;; proof-segment-upto-cmdstart (which becomes even more |
|---|
| 588 | ;; Isar specific, then...) |
|---|
| 589 | ;; (if (proof-string-match "\\.ML$" (buffer-name proof-script-buffer)) |
|---|
| 590 | ;; (format "ML_command {* %s *};" string) |
|---|
| 591 | ;; string) |
|---|
| 592 | (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string) |
|---|
| 593 | " \\<^sync>;")))) |
|---|
| 594 | |
|---|
| 595 | (defun isar-mode-config () |
|---|
| 596 | (isar-mode-config-set-variables) |
|---|
| 597 | (isar-init-syntax-table) |
|---|
| 598 | (setq font-lock-keywords isar-font-lock-keywords-1) |
|---|
| 599 | (setq comment-quote-nested nil) ;; can cope with nested comments |
|---|
| 600 | (proof-config-done) |
|---|
| 601 | (set (make-local-variable 'outline-regexp) isar-outline-regexp) |
|---|
| 602 | (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp) |
|---|
| 603 | (setq blink-matching-paren-dont-ignore-comments t) |
|---|
| 604 | (add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t) |
|---|
| 605 | (add-hook 'proof-shell-insert-hook 'isar-preprocessing)) |
|---|
| 606 | |
|---|
| 607 | (defun isar-shell-mode-config () |
|---|
| 608 | "Configure Proof General proof shell for Isabelle/Isar." |
|---|
| 609 | (isar-init-output-syntax-table) |
|---|
| 610 | (setq font-lock-keywords |
|---|
| 611 | (append |
|---|
| 612 | isar-output-font-lock-keywords-1 |
|---|
| 613 | (if (boundp 'x-symbol-isabelle-font-lock-keywords) |
|---|
| 614 | x-symbol-isabelle-font-lock-keywords))) |
|---|
| 615 | (isar-shell-mode-config-set-variables) |
|---|
| 616 | (proof-shell-config-done)) |
|---|
| 617 | |
|---|
| 618 | (defun isar-response-mode-config () |
|---|
| 619 | (isar-init-output-syntax-table) |
|---|
| 620 | (setq font-lock-keywords |
|---|
| 621 | (append |
|---|
| 622 | isar-output-font-lock-keywords-1 |
|---|
| 623 | (if (proof-ass x-symbol-enable) |
|---|
| 624 | x-symbol-isabelle-font-lock-keywords))) |
|---|
| 625 | (proof-response-config-done)) |
|---|
| 626 | |
|---|
| 627 | (defun isar-goals-mode-config () |
|---|
| 628 | ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO. |
|---|
| 629 | (setq pg-goals-change-goal "show %s.") |
|---|
| 630 | (setq pg-goals-error-regexp proof-shell-error-regexp) |
|---|
| 631 | (isar-init-output-syntax-table) |
|---|
| 632 | (setq font-lock-keywords |
|---|
| 633 | (append |
|---|
| 634 | isar-goals-font-lock-keywords |
|---|
| 635 | (if (proof-ass x-symbol-enable) |
|---|
| 636 | x-symbol-isabelle-font-lock-keywords))) |
|---|
| 637 | (proof-goals-config-done)) |
|---|
| 638 | |
|---|
| 639 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 640 | ;; |
|---|
| 641 | ;; Remove isa-mode from auto-mode-alist, |
|---|
| 642 | ;; to allow SML mode to work in preference to isa-mode. |
|---|
| 643 | ;; |
|---|
| 644 | |
|---|
| 645 | (setq auto-mode-alist |
|---|
| 646 | (delete-if |
|---|
| 647 | (lambda (strmod) (memq (cdr strmod) '(isa-mode demoisa-mode))) |
|---|
| 648 | auto-mode-alist)) |
|---|
| 649 | |
|---|
| 650 | (provide 'isar) |
|---|
