diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-12-20 14:42:21 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-12-20 14:42:21 +0100 |
commit | ebb55c998867fd13f8767a52a9542447347f7dc1 (patch) | |
tree | a2419396d62c3342e73e44099b8745d3201d09c7 /generic | |
parent | 0c9565d4d69a94cf33db5f98b381c3332709aa1e (diff) | |
parent | 883ce2ff1092003b6341cfebd1d7b2ab31239a41 (diff) |
Merge branch 'master' of github.com:ProofGeneral/PG
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-autotest.el | 9 | ||||
-rw-r--r-- | generic/pg-movie.el | 5 | ||||
-rw-r--r-- | generic/pg-pbrpm.el | 21 | ||||
-rw-r--r-- | generic/pg-user.el | 16 | ||||
-rw-r--r-- | generic/proof-depends.el | 4 | ||||
-rw-r--r-- | generic/proof-menu.el | 12 | ||||
-rw-r--r-- | generic/proof-script.el | 96 | ||||
-rw-r--r-- | generic/proof-splash.el | 4 | ||||
-rw-r--r-- | generic/proof-syntax.el | 14 | ||||
-rw-r--r-- | generic/proof-useropts.el | 4 | ||||
-rw-r--r-- | generic/proof-utils.el | 38 | ||||
-rw-r--r-- | generic/proof.el | 5 |
12 files changed, 112 insertions, 116 deletions
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index e7cb19a9..7a22c9f7 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -25,6 +25,7 @@ ;;; Code: +(eval-when-compile (require 'cl-lib)) (require 'proof-splash) (setq proof-splash-enable nil) ; prevent splash when testing @@ -215,7 +216,7 @@ completely processing the buffer as the last step." " random jump: processing whole buffer") (proof-process-buffer) (proof-shell-wait) - (decf jumps)) + (cl-decf jumps)) ((and (eq random-thing 1) (not (proof-locked-region-empty-p))) @@ -223,7 +224,7 @@ completely processing the buffer as the last step." " random jump: retracting whole buffer") (proof-retract-buffer) (proof-shell-wait) - (decf jumps)) + (cl-decf jumps)) (t (pg-autotest-message @@ -241,7 +242,7 @@ completely processing the buffer as the last step." " random jump: interrupting prover") (proof-interrupt-process))) (proof-shell-wait)) - (decf jumps))))) + (cl-decf jumps))))) (unless (proof-locked-region-full-p) (proof-process-buffer) (proof-shell-wait)) diff --git a/generic/pg-movie.el b/generic/pg-movie.el index 9be95972..755d41f5 100644 --- a/generic/pg-movie.el +++ b/generic/pg-movie.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -30,6 +30,7 @@ ;; ;;; Code: +(eval-when-compile (require 'cl-lib)) (eval-when-compile (require 'span) (require 'unicode-tokens)) @@ -72,7 +73,7 @@ (t "command"))) (label (span-property span 'rawname)) (frameid (int-to-string pg-movie-frame))) - (incf pg-movie-frame) + (cl-incf pg-movie-frame) (pg-xml-node frame (list (pg-xml-attr frameNumber frameid)) (list diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 619a5d6c..b40cfff3 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -34,6 +34,7 @@ ;;; Code: (require 'span) +(eval-when-compile (require 'cl-lib)) (eval-when-compile (require 'proof-utils)) @@ -377,10 +378,10 @@ Returns (n . s) where (while (and pos l (not found)) (setq start-goal (car l)) (setq end-goal (cadr l)) - (setq goal-name (caddr l)) - (setq start-concl (cadddr l)) - (setq hyps (car (cddddr l))) - (setq l (cdr (cddddr l))) + (setq goal-name (cl-caddr l)) + (setq start-concl (cl-cadddr l)) + (setq hyps (car (cl-cddddr l))) + (setq l (cdr (cl-cddddr l))) (if (and (<= start-goal pos) (<= pos end-goal)) (progn (setq found t) @@ -393,9 +394,9 @@ Returns (n . s) where (while (and hyps (not found)) (setq start-hyp (car hyps)) (setq start-hyp-text (cadr hyps)) - (setq end-hyp (caddr hyps)) - (setq hyp-name (cadddr hyps)) - (setq hyps (cddddr hyps)) + (setq end-hyp (cl-caddr hyps)) + (setq hyp-name (cl-cadddr hyps)) + (setq hyps (cl-cddddr hyps)) (if (and (<= start-hyp pos) (<= pos end-hyp)) (progn (setq found t) @@ -421,14 +422,14 @@ If no match found, return the empty string." (save-excursion (let ((pos (point))) (beginning-of-line) - (block 'loop + (cl-block 'loop (while (< (point) pos) (unless (search-forward-regexp pg-pbrpm-auto-select-regexp nil t) (return-from 'loop "")) (if (and (<= (match-beginning 0) pos) (<= pos (match-end 0))) - (return-from 'loop (match-string 0)))) - (return-from 'loop ""))))) + (cl-return-from 'loop (match-string 0)))) + (cl-return-from 'loop ""))))) (defun pg-pbrpm-translate-position (buffer pos) "If BUFFER is goals-buffer, return POS, otherwise the point in the goal buffer." diff --git a/generic/pg-user.el b/generic/pg-user.el index a5ed27a9..57d29f18 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -558,18 +558,18 @@ last use time, to discourage saving these into the users database." (defvar completion-min-length) (declare-function add-completion "completion" (string &optional num-uses last-use-time)) - (mapcar (lambda (cmpl) - ;; completion gives error; trapping is tricky so test again - (if (>= (length cmpl) completion-min-length) - (add-completion cmpl -1000 0))) - (proof-ass completion-table))) + (when proof-assistant + (mapcar (lambda (cmpl) + ;; completion gives error; trapping is tricky so test again + (if (>= (length cmpl) completion-min-length) + (add-completion cmpl -1000 0))) + (proof-ass completion-table)))) ;; NB: completion table is expected to be set when proof-script ;; is loaded! Call `proof-script-add-completions' to update. -(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck! - (eval-after-load "completion" - '(proof-add-completions))) +(eval-after-load "completion" + '(proof-add-completions)) (defun proof-script-complete (&optional arg) "Like `complete' but case-fold-search set to `proof-case-fold-search'." diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 9f3b469a..372ce06b 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -241,7 +241,7 @@ This is simply to display the dependency somehow." (defun proof-highlight-depcs (name nmspans) (let ((helpmsg (concat "This item is a dependency (ancestor) of " name))) (while nmspans - (let ((span (cadar nmspans))) + (let ((span (cl-cadar nmspans))) (proof-depends-save-old-face span) (span-set-property span 'face 'proof-highlight-dependency-face) ;; (span-set-property span 'priority pg-dep-span-priority) @@ -252,7 +252,7 @@ This is simply to display the dependency somehow." (defun proof-highlight-depts (name nmspans) (let ((helpmsg (concat "This item depends on (is a child of) " name))) (while nmspans - (let ((span (cadar nmspans))) + (let ((span (cl-cadar nmspans))) (proof-depends-save-old-face span) (span-set-property span 'face 'proof-highlight-dependent-face) ;; (span-set-property span 'priority pg-dep-span-priority) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index e43efcc0..dd3d05c8 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -793,7 +793,7 @@ suitable for adding to the proof assistant menu." (let* ((favs (proof-ass favourites)) (rmfavs (cl-remove-if - (lambda (f) (string-equal menuname (caddr f))) + (lambda (f) (string-equal menuname (cl-caddr f))) favs))) (unless (equal favs rmfavs) (easy-menu-remove-item proof-assistant-menu @@ -835,7 +835,7 @@ KEY is the optional key binding." ((menu-entry (proof-def-favourite command inscript menuname key t)) (favs (proof-ass favourites)) (rmfavs (cl-remove-if - (lambda (f) (string-equal menuname (caddr f))) + (lambda (f) (string-equal menuname (cl-caddr f))) favs)) (newfavs (append rmfavs @@ -864,11 +864,11 @@ KEY is the optional key binding." proof-assistant-settings) (dolist (grp (reverse groups)) (let* ((gstgs (cl-mapcan (lambda (stg) - (if (eq (get (car stg) 'pggroup) grp) - (list stg))) - proof-assistant-settings)) + (if (eq (get (car stg) 'pggroup) grp) + (list stg))) + proof-assistant-settings)) (cmds (mapcar (lambda (stg) - (apply 'proof-menu-entry-for-setting stg)) + (apply #'proof-menu-entry-for-setting stg)) (reverse gstgs)))) (setq ents (if grp (cons (cons grp cmds) ents) diff --git a/generic/proof-script.el b/generic/proof-script.el index 4c56fc7b..f8cf0cab 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1,4 +1,4 @@ -;;; proof-script.el --- Major mode for proof assistant script files. +;;; proof-script.el --- Major mode for proof assistant script files. -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -42,6 +42,7 @@ (declare-function proof-segment-up-to "proof-script") (declare-function proof-autosend-enable "pg-user") (declare-function proof-interrupt-process "pg-shell") +(declare-function proof-cd-sync "pg-user" ()) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -142,7 +143,7 @@ scripting buffer may have an active queue span.") ;; ** Getters and setters -(defun proof-span-give-warning (&rest args) +(defun proof-span-give-warning (&rest _args) "Give a warning message. Optional argument ARGS is ignored." (unless inhibit-read-only @@ -506,7 +507,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (defun pg-clear-script-portions () "Clear record of script portion names and types from internal list." (dolist (idtbl pg-script-portions) - (maphash (lambda (k span) (span-delete span)) (cdr idtbl)) + (maphash (lambda (_k span) (span-delete span)) (cdr idtbl)) (clrhash (cdr idtbl)))) (defun pg-remove-element (idiom id) @@ -628,14 +629,11 @@ IDIOMSYM is a symbol and ID is a strings." (concat "Make " (if current-prefix-arg "in" "") "visible all regions of: ") - (apply 'vector pg-idioms) nil t)) + (apply #'vector pg-idioms) nil t)) current-prefix-arg)) (let ((elts (cdr-safe (assq idiom pg-script-portions))) - (alterfn (if hide - (lambda (k span) - (pg-set-element-span-invisible span t)) - (lambda (k span) - (pg-set-element-span-invisible span nil))))) + (alterfn (lambda (_k span) + (pg-set-element-span-invisible span hide)))) (when elts (proof-with-script-buffer ; may be called from menu (maphash alterfn elts))))) @@ -668,7 +666,6 @@ Each span has a 'type property, one of: 'pbp A PBP command inserted automatically into the script." (let ((type (span-property span 'type)) (idiom (span-property span 'idiom)) - (name (span-property span 'name)) (rawname (span-property span 'rawname))) (cond (idiom @@ -1213,10 +1210,10 @@ activation is considered to have failed and an error is given." ;; If there's another buffer currently active, we need to ;; deactivate it (also fixing up the included files list). (when proof-script-buffer - (proof-deactivate-scripting) - ;; Test whether deactivation worked - (if proof-script-buffer - (error + (proof-deactivate-scripting) + ;; Test whether deactivation worked + (if proof-script-buffer + (error "You cannot have more than one active scripting buffer!"))) ;; Ensure this buffer is off the included files list. If we @@ -1265,21 +1262,21 @@ activation is considered to have failed and an error is given." ;; block. NB: The hook function may send commands to the ;; process which will re-enter this function, but should exit ;; immediately because scripting has been turned on now. - (if proof-activate-scripting-hook - (let - ((activated-interactively (called-interactively-p 'any))) - (setq proof-shell-last-output-kind nil) - (run-hooks 'proof-activate-scripting-hook) - ;; If activate scripting functions caused an error, - ;; prevent switching to another buffer. Might be better - ;; to leave to specific instances, or simply run the hooks - ;; as the last step before turning on scripting properly. - (when (or (eq 'error proof-shell-last-output-kind) - (eq 'interrupt proof-shell-last-output-kind)) - (proof-deactivate-scripting) ;; turn off again! - ;; Give an error to prevent further actions. - (error - "Scripting not activated because of error or interrupt"))))))) + (when proof-activate-scripting-hook + (defvar activated-interactively) + (let ((activated-interactively (called-interactively-p 'any))) + (setq proof-shell-last-output-kind nil) + (run-hooks 'proof-activate-scripting-hook) + ;; If activate scripting functions caused an error, + ;; prevent switching to another buffer. Might be better + ;; to leave to specific instances, or simply run the hooks + ;; as the last step before turning on scripting properly. + (when (or (eq 'error proof-shell-last-output-kind) + (eq 'interrupt proof-shell-last-output-kind)) + (proof-deactivate-scripting) ;; turn off again! + ;; Give an error to prevent further actions. + (error + "Scripting not activated because of error or interrupt"))))))) (defun proof-toggle-active-scripting (&optional arg) @@ -1415,7 +1412,8 @@ Argument SPAN has just been processed." (span-end span))) (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str) (condition-case nil - (eval (car (read-from-string (match-string-no-properties 1 str)))) + (eval (car (read-from-string (match-string-no-properties 1 str))) + t) (t (proof-debug (concat "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n" @@ -1599,7 +1597,7 @@ Subroutine of `proof-done-advancing-save'." ;; start of the buffer, we make a fake goal-save region. ;; Delete spans between the previous goal and new command - (mapc 'span-delete dels) + (mapc #'span-delete dels) ;; Try to set the name from the goal... [as above] (setq nam (or (proof-get-name-from-goal gspan) @@ -1643,7 +1641,7 @@ Subroutine of `proof-done-advancing-save'." ;; command syntax (terminated, not terminated, or lisp-style), whether ;; or not PG silently ignores comments, etc. -(defun proof-segment-up-to-parser (pos &optional next-command-end) +(defun proof-segment-up-to-parser (pos &optional _next-command-end) "Parse the script buffer from end of queue/locked region to POS. This partitions the script buffer into contiguous regions, classifying them by type. Return a list of lists of the form @@ -1838,7 +1836,7 @@ The optional QUEUEFLAGS are added to each queue item." (let ((start (proof-queue-or-locked-end)) (file (or (buffer-file-name) (buffer-name))) (cb 'proof-done-advancing) - span alist semi item end) + span alist end) (setq semis (nreverse semis)) (save-match-data (dolist (semi semis) @@ -1927,7 +1925,7 @@ always defaults to inserting a semi (nicer might be to parse for a comment, and insert or skip to the next semi)." (let ((mrk (point)) (termregexp (regexp-quote proof-terminal-string)) - ins incomment nwsp) + ins nwsp) (if (< mrk (proof-unprocessed-begin)) (insert proof-terminal-string) ; insert immediately in locked region (if (proof-only-whitespace-to-locked-region-p) @@ -1953,7 +1951,6 @@ comment, and insert or skip to the next semi)." (unless semis (error "Can't find a parseable command!")) (when (eq 'unclosed-comment (caar semis)) - (setq incomment t) ;; delete spurious char in comment (if ins (backward-delete-char 1)) (goto-char mrk) @@ -2258,17 +2255,22 @@ query saves here." ;; Proof General scripting mode definition, part 1. ;; +(defvar proof--splash-done nil) + ;;;###autoload (define-derived-mode proof-mode fundamental-mode proof-general-name "Proof General major mode class for proof scripts. \\{proof-mode-map}" + (unless (or proof--splash-done noninteractive) + (setq proof--splash-done t) + (proof-splash-message)) + (setq proof-buffer-type 'script) ;; Set default indent function (can be overriden in derived modes) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'proof-indent-line) + (setq-local indent-line-function #'proof-indent-line) ;; During write-file it can happen that we re-set the mode for the ;; currently active scripting buffer. The user might also do this @@ -2286,9 +2288,9 @@ query saves here." (proof-script-set-after-change-functions) (add-hook 'after-set-visited-file-name-hooks - 'proof-script-set-visited-file-name nil t) + #'proof-script-set-visited-file-name nil t) - (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)) + (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t)) ;; NB: proof-mode-map declared above (proof-menu-define-keys proof-mode-map) @@ -2321,9 +2323,9 @@ This hook also gives a warning in case this is the active scripting buffer." "Set the hooks for a proof script buffer. The hooks set here are cleared by `write-file', so we use this function to restore them using `after-set-visited-file-name-hooks'." - (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t) + (add-hook 'kill-buffer-hook #'proof-script-kill-buffer-fn t t) ;; Reverting buffer is same as killing it as far as PG is concerned - (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t)) + (add-hook 'before-revert-hook #'proof-script-kill-buffer-fn t t)) (defun proof-script-kill-buffer-fn () "Value of `kill-buffer-hook' for proof script buffers. @@ -2616,17 +2618,17 @@ finish setup which depends on specific proof assistant configuration." "Choose parsing mechanism according to different kinds of script syntax. Choice of function depends on configuration setting." (unless (fboundp 'proof-segment-up-to) - (defalias 'proof-segment-up-to 'proof-segment-up-to-parser) + (defalias 'proof-segment-up-to #'proof-segment-up-to-parser) (cond (proof-script-parse-function ;; already set, nothing to do ) (proof-script-sexp-commands - (setq proof-script-parse-function 'proof-script-generic-parse-sexp)) + (setq proof-script-parse-function #'proof-script-generic-parse-sexp)) (proof-script-command-start-regexp - (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart)) + (setq proof-script-parse-function #'proof-script-generic-parse-cmdstart)) ((or proof-script-command-end-regexp proof-terminal-string) - (setq proof-script-parse-function 'proof-script-generic-parse-cmdend) + (setq proof-script-parse-function #'proof-script-generic-parse-cmdend) (unless proof-script-command-end-regexp (proof-warn-if-unset "probof-config-done" 'proof-terminal-string) (setq proof-script-command-end-regexp @@ -2726,7 +2728,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.") (cdr semis)))) usedsemis))) -(defun proof-script-after-change-function (start end prelength) +(defun proof-script-after-change-function (start _end _prelength) "Value for `after-change-functions' in proof script buffers." (setq proof-last-edited-low-watermark (min (or proof-last-edited-low-watermark (point-max)) @@ -2741,7 +2743,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.") (defun proof-script-set-after-change-functions () "Set `after-change-functions' for script buffers." (add-hook 'after-change-functions - 'proof-script-after-change-function nil t)) + #'proof-script-after-change-function nil t)) diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 75164890..600e9b4e 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -270,7 +270,7 @@ binding to remove this buffer." (defun proof-splash-message () "Make sure the user gets welcomed one way or another." (interactive) - (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file)) + (unless (or proof-splash-seen noninteractive) (if proof-splash-enable (progn ;; disable ordinary emacs splash diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index e93f5ca4..d494279a 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -36,18 +36,14 @@ Uses a regexp of the form \\_<...\\_>." (defconst proof-no-regexp "\\<\\>" "A regular expression that never matches anything.") -(defsubst proof-regexp-alt (&rest args) +(defsubst proof-regexp-alt-list (args) "Return the regexp which matches any of the regexps ARGS." - ;; see regexp-opt (NB: but that is for strings, not regexps) - (let ((res "")) - (dolist (regexp args) - (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:") - regexp "\\)"))) - res)) + (mapconcat #'identity args "\\|")) -(defsubst proof-regexp-alt-list (args) +(defsubst proof-regexp-alt (&rest args) "Return the regexp which matches any of the regexps ARGS." - (apply 'proof-regexp-alt args)) + ;; see regexp-opt (NB: but that is for strings, not regexps) + (proof-regexp-alt-list args)) (defsubst proof-re-search-forward-region (startre endre) "Search for a region delimited by regexps STARTRE and ENDRE. diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 9a60e0ac..4ce51c99 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -50,7 +50,7 @@ approximation we test whether proof-config is fully-loaded yet." (set-default sym value) (when (and (not noninteractive) - (not (bound-and-true-p byte-compile-current-file)) + (not (bound-and-true-p byte-compile-current-file)) ;FIXME: Yuck! (featurep 'pg-custom) (featurep 'proof-config)) (if (fboundp sym) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 99e537c5..4a15301a 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -23,6 +23,7 @@ ;;; Code: +(eval-when-compile (require 'cl-lib)) ;; ;; Give Emacs version mismatch error here. ;; @@ -58,8 +59,6 @@ (require 'proof-autoloads) ; interface fns (require 'scomint) ; for proof-shell-live-buffer -;;; Code: - ;; ;; Handy macros ;; @@ -247,7 +246,8 @@ Experimentally we display a message from time to time advertising ;; IF there *isn't* a visible window showing buffer... (unless (get-buffer-window buffer 0) (if proof-three-window-enable - (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count) + (if (< proof-advertise-layout-count 30) + (cl-incf proof-advertise-layout-count) (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout")) (setq proof-advertise-layout-count 0))) ;; THEN either we are in 2 wins mode and we must switch the assoc @@ -589,25 +589,23 @@ The name of the defined function is returned." `(proof-deffloatset-fn (quote ,var) (quote ,othername))) (defun proof-defstringset-fn (var &optional othername) - "Define a function <VAR>-toggle for setting an integer customize setting VAR. -Args as for the macro `proof-defstringset', except will be evaluated." + "Define a function OTHERNAME for setting an string customize setting VAR. +OTHERNAME defaults to `VAR-stringset'." (eval - `(defun ,(if othername othername - (intern (concat (symbol-name var) "-stringset"))) (arg) - ,(concat "Set `" (symbol-name var) "' to ARG. -This function simply uses customize-set-variable to set the variable. + `(defun ,(or othername + (intern (concat (symbol-name var) "-stringset"))) + (arg) + ,(concat "Set `" (symbol-name var) "' to ARG. +This function simply uses `customize-set-variable' to set the variable. It was constructed with `proof-defstringset-fn'.") - (interactive ,(format "sValue for %s (a string): " - (symbol-name var))) - (customize-set-variable (quote ,var) arg)))) - -(defmacro proof-defstringset (var &optional othername) - "The setting function uses customize-set-variable to change the variable. -OTHERNAME gives an alternative name than the default <VAR>-stringset. -The name of the defined function is returned." - `(proof-defstringset-fn (quote ,var) (quote ,othername))) - - + (interactive (list + (read-string + (format "Value for %s (default %s): " + (symbol-name (quote ,var)) + (symbol-value (quote ,var))) + nil nil + (symbol-value (quote ,var))))) + (customize-set-variable (quote ,var) arg)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; diff --git a/generic/proof.el b/generic/proof.el index f3b3b276..769459df 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -1,4 +1,4 @@ -;;; proof.el --- Proof General theorem prover interface +;;; proof.el --- Proof General theorem prover interface -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -33,9 +33,6 @@ (require 'proof-site) ; site/prover config, global vars, autoloads -(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) - (proof-splash-message)) ; welcome the user now. - (require 'proof-utils) ; utilities (require 'proof-config) ; configuration variables (require 'proof-auxmodes) ; auxmode functions |