| 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, Makarius, 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 9.1 2008/02/04 12:52:10 da Exp $ |
|---|
| 15 | ;; |
|---|
| 16 | |
|---|
| 17 | ;;; Code: |
|---|
| 18 | (require 'proof) |
|---|
| 19 | |
|---|
| 20 | (eval-when-compile |
|---|
| 21 | (require 'span) |
|---|
| 22 | (require 'proof-syntax) |
|---|
| 23 | (proof-ready-for-assistant 'isar)) ; compile for isar |
|---|
| 24 | |
|---|
| 25 | (require 'isabelle-system) ; system code |
|---|
| 26 | (require 'isar-find-theorems) ; "Find Theorems" search form |
|---|
| 27 | |
|---|
| 28 | ;; |
|---|
| 29 | ;; Load syntax |
|---|
| 30 | ;; |
|---|
| 31 | (defcustom isar-keywords-name nil |
|---|
| 32 | "Specifies a theory-specific keywords setting to use with Isar. |
|---|
| 33 | See -k option for Isabelle interface script." |
|---|
| 34 | :type 'string |
|---|
| 35 | :group 'isabelle-isar) |
|---|
| 36 | |
|---|
| 37 | (or (featurep 'isar-keywords) |
|---|
| 38 | ;; Pickup isar-keywords file from somewhere appropriate, |
|---|
| 39 | ;; giving user chance to set name of file, or based on |
|---|
| 40 | ;; name of logic. |
|---|
| 41 | (isabelle-load-isar-keywords |
|---|
| 42 | (or isar-keywords-name |
|---|
| 43 | isabelle-chosen-logic))) |
|---|
| 44 | (require 'isar-syntax) |
|---|
| 45 | |
|---|
| 46 | |
|---|
| 47 | ;; Completion table for Isabelle/Isar identifiers |
|---|
| 48 | (defpgdefault completion-table isar-keywords-major) |
|---|
| 49 | |
|---|
| 50 | (defcustom isar-web-page |
|---|
| 51 | "http://isabelle.in.tum.de/Isar/" |
|---|
| 52 | "URL of web page for Isabelle/Isar." |
|---|
| 53 | :type 'string |
|---|
| 54 | :group 'isabelle-isar) |
|---|
| 55 | |
|---|
| 56 | |
|---|
| 57 | ;; Adjust toolbar entries (must be done before proof-toolbar is loaded). |
|---|
| 58 | |
|---|
| 59 | (eval-after-load "pg-custom" |
|---|
| 60 | '(setq isar-toolbar-entries |
|---|
| 61 | (remassoc 'qed (remassoc 'goal isar-toolbar-entries)))) |
|---|
| 62 | |
|---|
| 63 | |
|---|
| 64 | (defun isar-strip-terminators () |
|---|
| 65 | "Remove explicit Isabelle/Isar command terminators `;' from the buffer." |
|---|
| 66 | (interactive) |
|---|
| 67 | (save-excursion |
|---|
| 68 | (goto-char (point-min)) |
|---|
| 69 | (while (proof-search-forward ";" (point-max) t) |
|---|
| 70 | (if (not (proof-buffer-syntactic-context)) |
|---|
| 71 | (progn |
|---|
| 72 | (delete-backward-char 1) |
|---|
| 73 | (or (proof-looking-at ";\\|\\s-\\|$") |
|---|
| 74 | (insert " "))))))) |
|---|
| 75 | |
|---|
| 76 | |
|---|
| 77 | (defun isar-markup-ml (string) |
|---|
| 78 | "Return marked up version of ML command STRING for Isar." |
|---|
| 79 | (format "ML_command {* %s *};" string)) |
|---|
| 80 | |
|---|
| 81 | |
|---|
| 82 | (defun isar-mode-config-set-variables () |
|---|
| 83 | "Configure generic proof scripting mode variables for Isabelle/Isar." |
|---|
| 84 | (setq |
|---|
| 85 | proof-assistant-home-page isar-web-page |
|---|
| 86 | proof-prog-name (isabelle-command-line) |
|---|
| 87 | ;; proof script syntax |
|---|
| 88 | proof-terminal-char ?\; ; forcibly ends a command |
|---|
| 89 | proof-script-command-start-regexp |
|---|
| 90 | (proof-regexp-alt |
|---|
| 91 | ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *} |
|---|
| 92 | ;; because that's lexically a kind of comment. |
|---|
| 93 | isar-any-command-regexp |
|---|
| 94 | (regexp-quote ";")) |
|---|
| 95 | proof-script-integral-proofs t |
|---|
| 96 | ;; FIXME: use old parser for now to avoid { } problem |
|---|
| 97 | proof-script-use-old-parser t |
|---|
| 98 | proof-script-comment-start isar-comment-start |
|---|
| 99 | proof-script-comment-end isar-comment-end |
|---|
| 100 | proof-script-comment-start-regexp isar-comment-start-regexp |
|---|
| 101 | proof-script-comment-end-regexp isar-comment-end-regexp |
|---|
| 102 | proof-string-start-regexp isar-string-start-regexp |
|---|
| 103 | proof-string-end-regexp isar-string-end-regexp |
|---|
| 104 | |
|---|
| 105 | ;; Next few used for func-menu and recognizing goal..save regions in |
|---|
| 106 | ;; script buffer. |
|---|
| 107 | proof-save-command-regexp isar-save-command-regexp |
|---|
| 108 | proof-goal-command-regexp isar-goal-command-regexp |
|---|
| 109 | proof-goal-with-hole-regexp isar-named-entity-regexp |
|---|
| 110 | proof-goal-with-hole-result 2 |
|---|
| 111 | proof-save-with-hole-regexp nil |
|---|
| 112 | proof-script-next-entity-regexps isar-next-entity-regexps |
|---|
| 113 | proof-script-imenu-generic-expression isar-generic-expression |
|---|
| 114 | imenu-syntax-alist isar-script-syntax-table-alist |
|---|
| 115 | |
|---|
| 116 | proof-indent-enclose-offset (- proof-indent) |
|---|
| 117 | proof-indent-open-offset 0 |
|---|
| 118 | proof-indent-close-offset 0 |
|---|
| 119 | proof-indent-any-regexp isar-indent-any-regexp |
|---|
| 120 | ; proof-indent-inner-regexp isar-indent-inner-regexp |
|---|
| 121 | proof-indent-enclose-regexp isar-indent-enclose-regexp |
|---|
| 122 | proof-indent-open-regexp isar-indent-open-regexp |
|---|
| 123 | proof-indent-close-regexp isar-indent-close-regexp |
|---|
| 124 | |
|---|
| 125 | ;; proof engine commands |
|---|
| 126 | proof-showproof-command "pr" |
|---|
| 127 | proof-goal-command "lemma \"%s\"" |
|---|
| 128 | proof-save-command "qed" |
|---|
| 129 | proof-context-command "print_context" |
|---|
| 130 | proof-info-command "welcome" |
|---|
| 131 | proof-kill-goal-command "ProofGeneral.kill_proof" |
|---|
| 132 | ;; da: TODO: we should set this from our own setting, not suggest |
|---|
| 133 | ;; people customize prover-configuration variables |
|---|
| 134 | ; proof-find-theorems-command "find_theorems %s" ;; minibuffer |
|---|
| 135 | proof-find-theorems-command 'isar-find-theorems-minibuffer ;; equivalent |
|---|
| 136 | ; proof-find-theorems-command 'isar-find-theorems-form ;; search form |
|---|
| 137 | proof-shell-start-silent-cmd "disable_pr" |
|---|
| 138 | proof-shell-stop-silent-cmd "enable_pr" |
|---|
| 139 | proof-shell-trace-output-regexp "\375\\|\^AV" |
|---|
| 140 | ;; command hooks |
|---|
| 141 | proof-goal-command-p 'isar-goal-command-p |
|---|
| 142 | proof-really-save-command-p 'isar-global-save-command-p |
|---|
| 143 | proof-count-undos-fn 'isar-count-undos |
|---|
| 144 | proof-find-and-forget-fn 'isar-find-and-forget |
|---|
| 145 | proof-state-preserving-p 'isar-state-preserving-p |
|---|
| 146 | proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list |
|---|
| 147 | ;; span menu |
|---|
| 148 | proof-script-span-context-menu-extensions 'isabelle-create-span-menu)) |
|---|
| 149 | |
|---|
| 150 | (defun isar-shell-mode-config-set-variables () |
|---|
| 151 | "Configure generic proof shell mode variables for Isabelle/Isar." |
|---|
| 152 | (setq |
|---|
| 153 | pg-topterm-regexp "\376\\|\^AW" |
|---|
| 154 | |
|---|
| 155 | pg-topterm-goalhyplit-fn 'isar-goalhyplit-test |
|---|
| 156 | proof-shell-wakeup-char nil |
|---|
| 157 | proof-shell-annotated-prompt-regexp "^\\w*[>#] \372\\|^\\w*[>#] \^AS" |
|---|
| 158 | |
|---|
| 159 | ;; just for comint. |
|---|
| 160 | proof-shell-prompt-pattern "^\\w*[>#] " |
|---|
| 161 | |
|---|
| 162 | ;; for issuing command, not used to track cwd in any way. |
|---|
| 163 | proof-shell-cd-cmd (isar-markup-ml "ThyLoad.add_path \"%s\"") |
|---|
| 164 | |
|---|
| 165 | ;; Escapes for filenames inside ML strings. |
|---|
| 166 | ;; We also make a hack for a bug in Isabelle, by switching from |
|---|
| 167 | ;; backslashes to forward slashes if it looks like we're running |
|---|
| 168 | ;; on Windows. |
|---|
| 169 | proof-shell-filename-escapes |
|---|
| 170 | (if (fboundp 'win32-long-filename) ; rough test for XEmacs on win32 |
|---|
| 171 | ;; Patterns to unixfy names. |
|---|
| 172 | ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "") |
|---|
| 173 | ;; But I'll risk leaving drive names in, not sure how to replace them. |
|---|
| 174 | '(("\\\\" . "/") ("\"" . "\\\"")) |
|---|
| 175 | ;; Normal case: quotation for backslash, quote mark. |
|---|
| 176 | '(("\\\\" . "\\\\") ("\"" . "\\\""))) |
|---|
| 177 | |
|---|
| 178 | proof-shell-proof-completed-regexp nil ; n.a. |
|---|
| 179 | proof-shell-interrupt-regexp "\364\\*\\*\\* Interrupt\\|\^AM\\*\\*\\* Interrupt" |
|---|
| 180 | proof-shell-error-regexp "\364\\*\\*\\*\\|\^AM\\*\\*\\*" |
|---|
| 181 | proof-shell-abort-goal-regexp nil ; n.a. |
|---|
| 182 | |
|---|
| 183 | pg-next-error-regexp "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)" |
|---|
| 184 | pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)" |
|---|
| 185 | |
|---|
| 186 | ;; matches names of assumptions |
|---|
| 187 | proof-shell-assumption-regexp isar-id |
|---|
| 188 | |
|---|
| 189 | proof-shell-start-goals-regexp "\366\n\\|\^AO\n" |
|---|
| 190 | proof-shell-end-goals-regexp "\367\\|\^AP" |
|---|
| 191 | |
|---|
| 192 | proof-shell-init-cmd nil |
|---|
| 193 | proof-shell-restart-cmd "ProofGeneral.restart" |
|---|
| 194 | |
|---|
| 195 | proof-shell-eager-annotation-start-length 1 |
|---|
| 196 | proof-shell-eager-annotation-start "\360\\|\362\\|\^AI\\|\^AK" |
|---|
| 197 | proof-shell-eager-annotation-end "\361\\|\363\\|\^AJ\\|\^AL" |
|---|
| 198 | |
|---|
| 199 | ;; Isabelle is learning to talk PGIP... |
|---|
| 200 | proof-shell-match-pgip-cmd "<pgip" |
|---|
| 201 | proof-shell-issue-pgip-cmd 'isabelle-process-pgip |
|---|
| 202 | |
|---|
| 203 | ;; Some messages delimited by eager annotations |
|---|
| 204 | proof-shell-clear-response-regexp "Proof General, please clear the response buffer." |
|---|
| 205 | proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." |
|---|
| 206 | |
|---|
| 207 | ;; Theorem dependencies. NB: next regex anchored at end with eager annot end |
|---|
| 208 | proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\361\\|\^AJ\\)" |
|---|
| 209 | proof-shell-theorem-dependency-list-split "\" \"" |
|---|
| 210 | proof-shell-show-dependency-cmd "thm %s;" |
|---|
| 211 | proof-shell-identifier-under-mouse-cmd |
|---|
| 212 | '((nil "thm %s;") |
|---|
| 213 | (string "term \"%s\";") |
|---|
| 214 | (comment "term \"%s\";")) |
|---|
| 215 | |
|---|
| 216 | ;; Allow font-locking for output based on hidden annotations, see |
|---|
| 217 | ;; isar-output-font-lock-keywords-1 |
|---|
| 218 | pg-use-specials-for-fontify t |
|---|
| 219 | pg-after-fontify-output-hook 'pg-remove-specials |
|---|
| 220 | |
|---|
| 221 | pg-special-char-regexp |
|---|
| 222 | (if proof-shell-unicode "[0-9A-Z]" |
|---|
| 223 | ;; next string could be: "[\350-\377]", but that's buggy with XEmacs 21.5 (beta) |
|---|
| 224 | "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ") |
|---|
| 225 | |
|---|
| 226 | pg-subterm-help-cmd "term %s" |
|---|
| 227 | |
|---|
| 228 | proof-cannot-reopen-processed-files t |
|---|
| 229 | proof-shell-process-file |
|---|
| 230 | (cons |
|---|
| 231 | ;; Theory loader output |
|---|
| 232 | "Proof General, this file is loaded: \"\\(.*\\)\"" |
|---|
| 233 | (lambda (str) |
|---|
| 234 | (match-string 1 str))) |
|---|
| 235 | proof-shell-retract-files-regexp |
|---|
| 236 | "Proof General, you can unlock the file \"\\(.*\\)\"" |
|---|
| 237 | proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list |
|---|
| 238 | proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\"" |
|---|
| 239 | proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\"") |
|---|
| 240 | (add-hook 'proof-activate-scripting-hook 'isar-activate-scripting)) |
|---|
| 241 | |
|---|
| 242 | |
|---|
| 243 | ;;; |
|---|
| 244 | ;;; Theory loader operations |
|---|
| 245 | ;;; |
|---|
| 246 | |
|---|
| 247 | (defun isar-remove-file (name files cmp-base) |
|---|
| 248 | (if (not files) nil |
|---|
| 249 | (let* |
|---|
| 250 | ((file (car files)) |
|---|
| 251 | (rest (cdr files)) |
|---|
| 252 | (same (if cmp-base (string= name (file-name-nondirectory file)) |
|---|
| 253 | (string= name file)))) |
|---|
| 254 | (if same (isar-remove-file name rest cmp-base) |
|---|
| 255 | (cons file (isar-remove-file name rest cmp-base)))))) |
|---|
| 256 | |
|---|
| 257 | (defun isar-shell-compute-new-files-list (str) |
|---|
| 258 | "Compute the new list of files read by the proof assistant. |
|---|
| 259 | This is called when Proof General spots output matching |
|---|
| 260 | proof-shell-retract-files-regexp." |
|---|
| 261 | (let* |
|---|
| 262 | ((name (match-string 1 str)) |
|---|
| 263 | (base-name (file-name-nondirectory name))) |
|---|
| 264 | (if (string= name base-name) |
|---|
| 265 | (isar-remove-file name proof-included-files-list t) |
|---|
| 266 | (isar-remove-file (file-truename name) proof-included-files-list nil)))) |
|---|
| 267 | |
|---|
| 268 | (defun isar-activate-scripting () |
|---|
| 269 | "Make sure the Isabelle/Isar toplevel is in a sane state." |
|---|
| 270 | (proof-cd-sync)) |
|---|
| 271 | |
|---|
| 272 | |
|---|
| 273 | ;; |
|---|
| 274 | ;; Define the derived modes |
|---|
| 275 | ;; |
|---|
| 276 | (eval-and-compile |
|---|
| 277 | (define-derived-mode isar-shell-mode proof-shell-mode |
|---|
| 278 | "Isar shell" nil |
|---|
| 279 | (isar-shell-mode-config))) |
|---|
| 280 | |
|---|
| 281 | (eval-and-compile |
|---|
| 282 | (define-derived-mode isar-response-mode proof-response-mode |
|---|
| 283 | "response" nil |
|---|
| 284 | (isar-response-mode-config))) |
|---|
| 285 | |
|---|
| 286 | (eval-and-compile ; to define vars for byte comp. |
|---|
| 287 | (define-derived-mode isar-goals-mode proof-goals-mode |
|---|
| 288 | "proofstate" nil |
|---|
| 289 | (isar-goals-mode-config))) |
|---|
| 290 | |
|---|
| 291 | (eval-and-compile ; to define vars for byte comp. |
|---|
| 292 | (define-derived-mode isar-mode proof-mode |
|---|
| 293 | "Isar script" |
|---|
| 294 | "Major mode for editing Isar proof scripts. |
|---|
| 295 | |
|---|
| 296 | \\{isar-mode-map}" |
|---|
| 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 | (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)]) |
|---|
| 348 | |
|---|
| 349 | (defpgdefault menu-entries |
|---|
| 350 | (append |
|---|
| 351 | (list isabelle-logics-menu) |
|---|
| 352 | (list |
|---|
| 353 | (cons "Commands" |
|---|
| 354 | (list |
|---|
| 355 | ["refute" isar-cmd-refute t] |
|---|
| 356 | ["quickcheck" isar-cmd-quickcheck t] |
|---|
| 357 | ["sledgehammer" isar-cmd-sledgehammer t] |
|---|
| 358 | ["display draft" isar-cmd-display-draft t]))) |
|---|
| 359 | (list |
|---|
| 360 | (cons "Show me ..." |
|---|
| 361 | (list |
|---|
| 362 | ["cases" isar-help-cases t] |
|---|
| 363 | ["facts" isar-help-facts t] |
|---|
| 364 | ["term bindings" isar-help-binds t] |
|---|
| 365 | "----" |
|---|
| 366 | ["classical rules" isar-help-claset t] |
|---|
| 367 | ["induct/cases rules" isar-help-induct-rules t] |
|---|
| 368 | ["simplifier rules" isar-help-simpset t] |
|---|
| 369 | ["theorems" isar-help-theorems t] |
|---|
| 370 | ["transitivity rules" isar-help-trans-rules t] |
|---|
| 371 | "----" |
|---|
| 372 | ["antiquotations" isar-help-antiquotations t] |
|---|
| 373 | ["attributes" isar-help-attributes t] |
|---|
| 374 | ["commands" isar-help-commands t] |
|---|
| 375 | ["inner syntax" isar-help-syntax t] |
|---|
| 376 | ["methods" isar-help-methods t]))))) |
|---|
| 377 | |
|---|
| 378 | ;; undo proof commands |
|---|
| 379 | (defun isar-count-undos (span) |
|---|
| 380 | "Count number of undos SPAN, return command needed to undo that far." |
|---|
| 381 | (let |
|---|
| 382 | ((case-fold-search nil) ;FIXME ?? |
|---|
| 383 | (ct 0) str i) |
|---|
| 384 | (while span |
|---|
| 385 | (setq str (or (span-property span 'cmd) "")) |
|---|
| 386 | (cond ((eq (span-property span 'type) 'vanilla) |
|---|
| 387 | (or (proof-string-match isar-undo-skip-regexp str) |
|---|
| 388 | (proof-string-match isar-undo-ignore-regexp str) |
|---|
| 389 | (setq ct (+ 1 ct)))) |
|---|
| 390 | ((eq (span-property span 'type) 'pbp) |
|---|
| 391 | ;; this case for automatically inserted text (e.g. sledgehammer) |
|---|
| 392 | (cond ((not (proof-string-match isar-undo-skip-regexp str)) |
|---|
| 393 | (setq ct 1) |
|---|
| 394 | (setq i 0) |
|---|
| 395 | ;; If we find a semicolon, assume several commands, |
|---|
| 396 | ;; and increment the undo count. |
|---|
| 397 | (while (< i (length str)) |
|---|
| 398 | (if (= (aref str i) proof-terminal-char) |
|---|
| 399 | (setq ct (+ 1 ct))) |
|---|
| 400 | (setq i (+ 1 i)))) |
|---|
| 401 | (t nil)))) |
|---|
| 402 | (setq span (next-span span 'type))) |
|---|
| 403 | (isar-undos ct))) |
|---|
| 404 | |
|---|
| 405 | ;; undo theory commands |
|---|
| 406 | (defun isar-find-and-forget (span) |
|---|
| 407 | "Return commands to be used to forget SPAN." |
|---|
| 408 | (let (str ans answers) |
|---|
| 409 | (while span |
|---|
| 410 | (setq str (or (span-property span 'cmd) "")) |
|---|
| 411 | (setq ans nil) |
|---|
| 412 | (cond |
|---|
| 413 | ;; comment, diagnostic, nested proof command: skip |
|---|
| 414 | ;; (da: adding new span types may break this code, |
|---|
| 415 | ;; ought to test for type 'cmd before looking at |
|---|
| 416 | ;; str below) |
|---|
| 417 | ;; FIXME: should adjust proof-nesting-depth here. |
|---|
| 418 | ((or (eq (span-property span 'type) 'comment) |
|---|
| 419 | (eq (span-property span 'type) 'proverproc) |
|---|
| 420 | (eq (span-property span 'type) 'proof); da: needed? |
|---|
| 421 | (proof-string-match isar-undo-skip-regexp str) |
|---|
| 422 | (proof-string-match isar-undo-ignore-regexp str))) |
|---|
| 423 | ;; finished goal: undo |
|---|
| 424 | ((eq (span-property span 'type) 'goalsave) |
|---|
| 425 | (setq ans isar-undo)) |
|---|
| 426 | ;; open goal: skip and exit |
|---|
| 427 | ((proof-string-match isar-goal-command-regexp str) |
|---|
| 428 | (setq span nil)) |
|---|
| 429 | ;; control command: cannot undo |
|---|
| 430 | ((and (proof-string-match isar-undo-fail-regexp str)) |
|---|
| 431 | (setq ans (isar-cannot-undo (match-string 1 str))) |
|---|
| 432 | (setq answers nil) |
|---|
| 433 | (setq span nil)) |
|---|
| 434 | ;; theory: remove and exit |
|---|
| 435 | ((proof-string-match isar-undo-remove-regexp str) |
|---|
| 436 | (setq ans (isar-remove (match-string 2 str))) |
|---|
| 437 | (setq span nil)) |
|---|
| 438 | ;; else: undo |
|---|
| 439 | (t |
|---|
| 440 | (setq ans isar-undo))) |
|---|
| 441 | (if ans (setq answers (cons ans answers))) |
|---|
| 442 | (if span (setq span (next-span span 'type)))) |
|---|
| 443 | (if (null answers) proof-no-command (apply 'concat answers)))) |
|---|
| 444 | |
|---|
| 445 | (defun isar-goal-command-p (span) |
|---|
| 446 | "Decide whether argument SPAN is a goal or not." |
|---|
| 447 | (proof-string-match isar-goal-command-regexp |
|---|
| 448 | (or (span-property span 'cmd) ""))) |
|---|
| 449 | |
|---|
| 450 | (defun isar-global-save-command-p (span str) |
|---|
| 451 | "Decide whether argument SPAN with command STR is a global save command." |
|---|
| 452 | (or |
|---|
| 453 | (proof-string-match isar-global-save-command-regexp str) |
|---|
| 454 | (let ((ans nil) (lev 0) cmd) |
|---|
| 455 | (while (and (not ans) span (setq span (prev-span span 'type))) |
|---|
| 456 | (setq cmd (or (span-property span 'cmd) "")) |
|---|
| 457 | (cond |
|---|
| 458 | ;; comment: skip |
|---|
| 459 | ((eq (span-property span 'type) 'comment)) |
|---|
| 460 | ;; local qed: enter block |
|---|
| 461 | ((proof-string-match isar-save-command-regexp cmd) |
|---|
| 462 | (setq lev (+ lev 1))) |
|---|
| 463 | ;; local goal: leave block, or done |
|---|
| 464 | ((proof-string-match isar-local-goal-command-regexp cmd) |
|---|
| 465 | (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) |
|---|
| 466 | ;; global goal: done |
|---|
| 467 | ((proof-string-match isar-goal-command-regexp cmd) |
|---|
| 468 | (setq ans 'yes)))) |
|---|
| 469 | (eq ans 'yes)))) |
|---|
| 470 | |
|---|
| 471 | (defvar isar-current-goal 1 |
|---|
| 472 | "Last goal that Emacs looked at.") |
|---|
| 473 | |
|---|
| 474 | (defun isar-state-preserving-p (cmd) |
|---|
| 475 | "Non-nil if command CMD preserves the proofstate." |
|---|
| 476 | (proof-string-match isar-undo-skip-regexp cmd)) |
|---|
| 477 | |
|---|
| 478 | |
|---|
| 479 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 480 | ;; Commands specific to isar ;; |
|---|
| 481 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 482 | |
|---|
| 483 | (proof-defshortcut isar-bold "\\<^bold>%p" [(control b)]) |
|---|
| 484 | (proof-defshortcut isar-local "\\<^loc>%p" [(control c)]) |
|---|
| 485 | (proof-defshortcut isar-super "\\<^sup>%p" [(control u)]) |
|---|
| 486 | (proof-defshortcut isar-sub "\\<^sub>%p" [(control l)]) |
|---|
| 487 | (proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [?u]) |
|---|
| 488 | (proof-defshortcut isar-longsub "\\<^bsub>%p\\<^esub>" [?l]) |
|---|
| 489 | (proof-defshortcut isar-idsub "\\<^isub>%p" [(control i)]) |
|---|
| 490 | (proof-defshortcut isar-raw "\\<^raw:%p>" [(control r)]) |
|---|
| 491 | (proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)]) |
|---|
| 492 | (proof-defshortcut isar-ml "ML {* %p *}" [(control x)]) |
|---|
| 493 | |
|---|
| 494 | |
|---|
| 495 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 496 | ;; Isar shell startup and exit hooks ;; |
|---|
| 497 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
|---|
| 498 | |
|---|
| 499 | (defvar isar-shell-current-line-width nil |
|---|
| 500 | "Current line width of the Isabelle process's pretty printing module. |
|---|
| 501 | Its value will be updated whenever the corresponding screen gets |
|---|
| 502 | selected.") |
|---|
| 503 | |
|---|
| 504 | (defun isar-shell-adjust-line-width () |
|---|
| 505 | "Use Isabelle's pretty printing facilities to adjust output line width. |
|---|
| 506 | Checks the width in the `proof-goals-buffer'" |
|---|
| 507 | (let ((ans "")) |
|---|
| 508 | (and (buffer-live-p proof-goals-buffer) |
|---|
| 509 | (proof-shell-live-buffer) |
|---|
| 510 | (save-excursion |
|---|
| 511 | (set-buffer proof-goals-buffer) |
|---|
| 512 | (let ((current-width |
|---|
| 513 | ;; Actually, one might want the width of the |
|---|
| 514 | ;; proof-response-buffer instead. Never mind. |
|---|
| 515 | (max 20 (window-width (get-buffer-window proof-goals-buffer t))))) |
|---|
| 516 | |
|---|
| 517 | (if (equal current-width isar-shell-current-line-width) () |
|---|
| 518 | (setq isar-shell-current-line-width current-width) |
|---|
| 519 | (set-buffer proof-shell-buffer) |
|---|
| 520 | (setq ans (format "pretty_setmargin %d;" (- current-width 4))))))) |
|---|
| 521 | ans)) |
|---|
| 522 | |
|---|
| 523 | ;; |
|---|
| 524 | ;; Configuring proof output buffer |
|---|
| 525 | ;; |
|---|
| 526 | |
|---|
| 527 | (defconst isar-command-nesting-available |
|---|
| 528 | (member "Isabelle\\.command" isar-keywords-major)) |
|---|
| 529 | |
|---|
| 530 | (defun isar-command-wrapping (string) |
|---|
| 531 | (if (and isar-command-nesting-available |
|---|
| 532 | (not (proof-string-match "^ProofGeneral\\.process_pgip" string))) |
|---|
| 533 | (concat |
|---|
| 534 | "Isabelle.command \"" |
|---|
| 535 | (proof-replace-regexp-in-string |
|---|
| 536 | "[\000-\037\"\\\\]" |
|---|
| 537 | (lambda (str) (format "\\\\%03d" (string-to-char str))) |
|---|
| 538 | string) |
|---|
| 539 | "\"") |
|---|
| 540 | (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string))) |
|---|
| 541 | |
|---|
| 542 | (defun isar-preprocessing () ;dynamic scoping of `string' |
|---|
| 543 | "Isabelle command wrapping - acts on variable STRING by dynamic scoping." |
|---|
| 544 | (if (proof-string-match isabelle-verbatim-regexp string) |
|---|
| 545 | (setq string (match-string 1 string)) |
|---|
| 546 | (unless (proof-string-match ";[ \t]*\\'" string) |
|---|
| 547 | (setq string (concat string ";"))) |
|---|
| 548 | (setq string (concat |
|---|
| 549 | " \\<^sync>; " |
|---|
| 550 | (isar-shell-adjust-line-width) |
|---|
| 551 | (isar-command-wrapping string) |
|---|
| 552 | " \\<^sync>;")))) |
|---|
| 553 | |
|---|
| 554 | (defun isar-mode-config () |
|---|
| 555 | (isar-mode-config-set-variables) |
|---|
| 556 | (isar-init-syntax-table) |
|---|
| 557 | (setq font-lock-keywords isar-font-lock-keywords-1) |
|---|
| 558 | (setq comment-quote-nested nil) ;; can cope with nested comments |
|---|
| 559 | (set (make-local-variable 'outline-regexp) isar-outline-regexp) |
|---|
| 560 | (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp) |
|---|
| 561 | (setq blink-matching-paren-dont-ignore-comments t) |
|---|
| 562 | (add-hook 'proof-shell-insert-hook 'isar-preprocessing) |
|---|
| 563 | (proof-config-done)) |
|---|
| 564 | |
|---|
| 565 | (defun isar-shell-mode-config () |
|---|
| 566 | "Configure Proof General proof shell for Isabelle/Isar." |
|---|
| 567 | (isar-init-output-syntax-table) |
|---|
| 568 | (setq font-lock-keywords |
|---|
| 569 | (append |
|---|
| 570 | isar-output-font-lock-keywords-1 |
|---|
| 571 | (if (boundp 'x-symbol-isar-font-lock-keywords) |
|---|
| 572 | x-symbol-isar-font-lock-keywords))) |
|---|
| 573 | (isar-shell-mode-config-set-variables) |
|---|
| 574 | (proof-shell-config-done)) |
|---|
| 575 | |
|---|
| 576 | (defun isar-response-mode-config () |
|---|
| 577 | (isar-init-output-syntax-table) |
|---|
| 578 | (setq font-lock-keywords |
|---|
| 579 | (append |
|---|
| 580 | isar-output-font-lock-keywords-1 |
|---|
| 581 | (if isar-x-symbol-enable |
|---|
| 582 | x-symbol-isar-font-lock-keywords))) |
|---|
| 583 | (proof-response-config-done)) |
|---|
| 584 | |
|---|
| 585 | (defun isar-goals-mode-config () |
|---|
| 586 | (setq pg-goals-change-goal "prefer %s") |
|---|
| 587 | (setq pg-goals-error-regexp proof-shell-error-regexp) |
|---|
| 588 | (isar-init-output-syntax-table) |
|---|
| 589 | (setq font-lock-keywords |
|---|
| 590 | (append |
|---|
| 591 | isar-goals-font-lock-keywords |
|---|
| 592 | (if isar-x-symbol-enable |
|---|
| 593 | x-symbol-isar-font-lock-keywords))) |
|---|
| 594 | (proof-goals-config-done)) |
|---|
| 595 | |
|---|
| 596 | (defun isar-goalhyplit-test () |
|---|
| 597 | "Value for `pg-topterm-goalhyplit-fn' (see that variable for documentation)." |
|---|
| 598 | (let ((start (point))) |
|---|
| 599 | (if (proof-re-search-forward |
|---|
| 600 | "\377\\|\^AX" nil t) ; end of literal command (non-standard) |
|---|
| 601 | (progn |
|---|
| 602 | (delete-region (match-beginning 0) (match-end 0)) |
|---|
| 603 | (cons 'lit (buffer-substring start (match-beginning 0))))))) |
|---|
| 604 | |
|---|
| 605 | |
|---|
| 606 | (provide 'isar) |
|---|
| 607 | |
|---|
| 608 | ;;; isar.el ends here |
|---|
