diff options
| -rw-r--r-- | generic/proof-script.el | 54 | ||||
| -rw-r--r-- | isa/isa.el | 15 |
2 files changed, 42 insertions, 27 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 2b6e92ae..3087fcfc 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -149,6 +149,7 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding (make-variable-buffer-local 'proof-queue-span) (defun proof-init-segmentation () + "Initialise the spans in a proof script buffer." (setq proof-queue-loose-end nil) (if (not proof-queue-span) (setq proof-queue-span (make-span 1 1))) @@ -224,7 +225,8 @@ buffer to END." "Return end of locked region in current buffer or (point-min) otherwise." (or (and (member (current-buffer) proof-script-buffer-list) - proof-locked-span (span-end proof-locked-span)) + proof-locked-span + (span-end proof-locked-span)) (point-min))) (defun proof-locked-end () @@ -255,30 +257,42 @@ Only call this from a scripting buffer." "Mark BUFFER as having been processed in a single step. If buffer already contains a locked region, only the remainder of the -buffer is closed off atomically." +buffer is closed off atomically. + +This works for buffers which are not in proof scripting mode too, +to allow other files loaded by proof assistants to be marked read-only." (save-excursion (set-buffer buffer) (let ((span (make-span (proof-unprocessed-begin) (point-max))) cmd) - ;; compute first command of buffer - (goto-char (point-min)) - (proof-find-next-terminator) - (let ((cmd-list (member-if - (lambda (entry) (equal (car entry) 'cmd)) - (proof-segment-up-to (point))))) + (if (eq proof-buffer-type 'script) + ;; For a script buffer + (progn + (goto-char (point-min)) + (proof-find-next-terminator) + (let ((cmd-list (member-if + (lambda (entry) (equal (car entry) 'cmd)) + (proof-segment-up-to (point))))) + ;; FIXME: should -init- be done if spans already exist? + (proof-init-segmentation) + (if cmd-list + (progn + (setq cmd (second (car cmd-list))) + (set-span-property span 'type 'vanilla) + (set-span-property span 'cmd cmd)) + ;; If there was no command in the buffer, atomic + ;; span becomes a comment. + (set-span-property span 'type 'comment))) + ;; Make sure a new proof script buffer enters the list + ;; of script buffers. + (or (member buffer proof-script-buffer-list) + (setq proof-script-buffer-list + (append proof-script-buffer-list (list buffer))))) + ;; For a non-script buffer (proof-init-segmentation) - (if cmd-list - (progn - (setq cmd (second (car cmd-list))) - (set-span-property span 'type 'vanilla) - (set-span-property span 'cmd cmd)) - ;; If there was no command in the buffer, atomic - ;; span becomes a comment. - (set-span-property span 'type 'comment))) - (proof-set-locked-end (point-max)) - (or (member buffer proof-script-buffer-list) - (setq proof-script-buffer-list - (append proof-script-buffer-list (list buffer))))))) + (set-span-property span 'type 'comment)) + ;; End of locked region is always end of buffer + (proof-set-locked-end (point-max))))) (defun proof-file-truename (filename) "Returns the true name of the file FILENAME or nil." @@ -140,12 +140,8 @@ no regular or easily discernable structure." ;; Theory loader output and verbose update() output. "Reading \"\\(.*\\)\"\\|Not reading \"\\(.*\\)\"" (lambda (str) - (let ((filename (or (match-string 1 str) - (match-string 2 str)))) - (if (string-match "\\.ML$" filename) - filename) - ;; Ignore .thy files for now - ))) + (or (match-string 1 str) + (match-string 2 str)))) ;; This is the output returned by a special command to ;; query Isabelle for outdated files. proof-shell-retract-files-regexp @@ -243,8 +239,13 @@ isa-proofscript-mode." (interactive) (cond ((string-match ".thy" (buffer-file-name)) - (thy-mode)) + (thy-mode) + ;; Has this theory file been loaded by Isabelle? + ;; Colour it blue if so. + (and (member buffer-file-truename proof-included-files-list) + (proof-mark-buffer-atomic (current-buffer)))) (t + ;; Proof mode does this automatically. (isa-proofscript-mode)))) ;; Next portion taken from isa-load.el |