diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2009-09-09 23:13:01 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-09 23:13:01 +0000 |
commit | 41542208cdf5437bf7604d042779d5ac9d7684a8 (patch) | |
tree | 0e621d636eeea579ef82a605f1c4a3203a116034 /isar | |
parent | f1dc2bd435c9bb6442925b314198f312bc60c0ee (diff) |
Support linear_undo. Add minimal font-lock for readability in *isabelle*.
Diffstat (limited to 'isar')
-rw-r--r-- | isar/isar-syntax.el | 8 | ||||
-rw-r--r-- | isar/isar.el | 41 |
2 files changed, 35 insertions, 14 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 2e024eac..83d879a5 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -418,6 +418,9 @@ matches contents of quotes for quoted identifiers.") "Remove invisible output markup from STRING" (replace-regexp-in-string "\^A." "" string)) +(defconst isar-shell-font-lock-keywords + '(("\^A." (0 '(face nil invisible t))))) + (defvar isar-goals-font-lock-keywords (append (list @@ -459,8 +462,9 @@ matches contents of quotes for quoted identifiers.") (defun isar-remove (name) (concat "init_toplevel; kill_thy " name ";")) -(defun isar-undos (i) - (if (> i 0) (concat "undos_proof " (int-to-string i) ";") +(defun isar-undos (linearp i) + (if (> i 0) (concat (if linearp "linear_undo " "undos_proof ") + (int-to-string i) ";") nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) diff --git a/isar/isar.el b/isar/isar.el index 19abfedc..52598abc 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -141,21 +141,19 @@ See -k option for Isabelle interface script." '((nil "thm %s;") (string "term \"%s\";") (comment "term \"%s\";")) - proof-kill-goal-command "ProofGeneral.kill_proof" proof-shell-start-silent-cmd "disable_pr" proof-shell-stop-silent-cmd "enable_pr" proof-shell-trace-output-regexp "\^AI\^AV" ;; command hooks proof-goal-command-p 'isar-goal-command-p proof-really-save-command-p 'isar-global-save-command-p - proof-count-undos-fn 'isar-count-undos - proof-find-and-forget-fn 'isar-find-and-forget proof-state-preserving-p 'isar-state-preserving-p proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list ;; span menu proof-script-span-context-menu-extensions 'isabelle-create-span-menu) ;; proof assistant settings (setq proof-use-pgip-askprefs t) + ;; others: find theorems, undo config (isar-configure-from-settings)) (defun isar-shell-mode-config-set-variables () @@ -239,10 +237,6 @@ See -k option for Isabelle interface script." ;;; (Settings for Isabelle are configured automatically via PGIP message) ;;; - -(defun isar-configure-from-settings () - (isar-set-proof-find-theorems-command)) - (defpacustom use-find-theorems-form nil "Use a form-style input for the find theorems operation." :type 'boolean @@ -254,6 +248,25 @@ See -k option for Isabelle interface script." 'isar-find-theorems-form 'isar-find-theorems-minibuffer))) +(defpacustom use-linear-undo t + "Whether to allow undo to re-enter completed proofs (requires restart)." + :type 'boolean) + +(defun isar-set-undo-commands () + (setq proof-count-undos-fn 'isar-count-undos) + (when isar-linear-undo + (setq proof-kill-goal-command nil) + (setq proof-find-and-forget-fn 'isar-count-undos) + (setq proof-arbitrary-undo-positions t)) + (when (not isar-linear-undo) + (setq proof-kill-goal-command "ProofGeneral.kill_proof") + (setq proof-find-and-forget-fn 'isar-find-and-forget) + (setq proof-arbitrary-undo-positions nil))) + +(defun isar-configure-from-settings () + (isar-set-proof-find-theorems-command) + (isar-set-undo-commands)) + ;;; ;;; Theory loader operations ;;; @@ -394,12 +407,12 @@ This is called when Proof General spots output matching ;; undo proof commands (defun isar-count-undos (span) - "Count number of undos SPAN, return command needed to undo that far." - (let - ((ct 0) str i) + "Return commands to be used to forget SPAN." + (let ((ct 0) str i) (while span (setq str (or (span-property span 'cmd) "")) - (cond ((eq (span-property span 'type) 'vanilla) + (cond ((or (eq (span-property span 'type) 'vanilla) + (eq (span-property span 'type) 'goalsave)) (or (proof-string-match isar-undo-skip-regexp str) (proof-string-match isar-undo-ignore-regexp str) (setq ct (+ 1 ct)))) @@ -416,7 +429,7 @@ This is called when Proof General spots output matching (setq i (+ 1 i)))) (t nil)))) (setq span (next-span span 'type))) - (isar-undos ct))) + (isar-undos isar-use-linear-undo ct))) ;; undo theory commands (defun isar-find-and-forget (span) @@ -624,6 +637,10 @@ Uses variables `string' and `scriptspan' passed by dynamic scoping." "Configure Proof General proof shell for Isabelle/Isar." (isar-init-output-syntax-table) (isar-shell-mode-config-set-variables) + (set (make-local-variable 'font-lock-extra-managed-props) + '(invisible)) + (setq proof-shell-font-lock-keywords + isar-shell-font-lock-keywords) (proof-shell-config-done)) (defun isar-response-mode-config () |