branch: elpa/proof-general
commit d64f5a10bc4747f04b4ae908f88c21ae7f452495
Author: Stefan Monnier <monn...@iro.umontreal.ca>
Commit: Stefan Monnier <monn...@iro.umontreal.ca>
* generic/*.el: Use lexical-binding in proof-(tree|splash|pg-pamacs)
Plus various minor changes found along the way.
* generic/proof-tree.el: Use lexical-binding.
(proof-tree-insert-script, proof-tree-make-show-goal-callback):
Prefer closures over `(lambda...).
(proof-tree-handle-proof-command): Remove unused var `proof-state`.
* generic/proof-splash.el: Use lexical-binding.
(proof-splash-message): Prefer closures over `(lambda...).
* generic/proof-site.el (proof-assistants): Use `mapconcat` and quote
symbols using the ELisp docstring convention.
* generic/proof-script.el (pg-add-element): Prefer closures over
`(lambda...).
(proof-config-done): Remove calls to `easy-menu-add` since we don't
support XEmacs any more.
* generic/proof-depends.el (proof-dependency-in-span-context-menu):
Simplify by eta-reduction.
(proof-dep-make-submenu): Prefer closures over `(lambda...).
* generic/pg-pamacs.el: Use lexical-binding.
(proof-defpgcustom-fn): Remove unused var `newargs`. Simplify a bit
using `push` and `memq`.
---
generic/pg-pamacs.el | 46 ++++++++++++++++++++++++----------------------
generic/proof-depends.el | 25 +++++++++++++------------
generic/proof-script.el | 24 +++++++++++-------------
generic/proof-site.el | 24 ++++++++++++++----------
generic/proof-splash.el | 27 +++++++++++++--------------
generic/proof-tree.el | 30 +++++++++++++++---------------
6 files changed, 90 insertions(+), 86 deletions(-)
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 1492e0c..c603d15 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -1,9 +1,9 @@
-;;; pg-pamacs.el --- Macros for per-proof assistant configuration
+;;; pg-pamacs.el --- Macros for per-proof assistant configuration -*-
lexical-binding: t; -*-
;; 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-2021 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
@@ -75,7 +75,7 @@ This macro should only be invoked once a specific prover is
engaged."
(defun proof-ass-differs-from-default (sym)
"Return non-nil if SYM for current prover differs from its customize
standard value."
(let ((pasym (proof-ass-symv sym)))
- (not (equal (eval (car (get pasym 'standard-value)))
+ (not (equal (eval (car (get pasym 'standard-value)) t)
(symbol-value pasym)))))
(defun proof-defpgcustom-fn (sym args)
@@ -83,14 +83,16 @@ This macro should only be invoked once a specific prover is
engaged."
Helper for macro `defpgcustom'."
(let ((specific-var (proof-ass-symv sym))
(generic-var (intern (concat "proof-assistant-" (symbol-name sym))))
- (newargs (if (member :group args)
- args
- (append (list :group
- proof-assistant-internals-cusgrp)
- args))))
+ ;; (newargs (if (member :group args)
+ ;; args
+ ;; (append (list :group
+ ;; proof-assistant-internals-cusgrp)
+ ;; args)))
+ )
(eval
`(defcustom ,specific-var
- ,@args))
+ ,@args)
+ t)
;; For functions, we could simply use defalias. Unfortunately there
;; is nothing similar for values, so we define a new set/get function.
(eval
@@ -100,7 +102,8 @@ Helper for macro `defpgcustom'."
If NEWVAL is present, set the variable, otherwise return its current value.")
(if newval
(setq ,specific-var newval)
- ,specific-var)))))
+ ,specific-var))
+ t)))
(defun undefpgcustom (sym)
(let ((specific-var (proof-ass-symv sym))
@@ -188,7 +191,7 @@ Usage: (defpgdefault SYM VALUE)"
(setq args (cdr args)))
((eq (car args) :type)
(setq type (cadr args))
- (if (eq (eval type) 'float)
+ (if (eq (eval type t) 'float)
(setq type (quote 'number))) ; widget type for defcustom
(setq args (cdr args))
(setq newargs (cons type (cons :type newargs))))
@@ -198,10 +201,7 @@ Usage: (defpgdefault SYM VALUE)"
(setq newargs (reverse newargs))
(setq descr (car-safe newargs))
(unless (and type
- (or (eq (eval type) 'boolean)
- (eq (eval type) 'integer)
- (eq (eval type) 'number)
- (eq (eval type) 'string)))
+ (memq (eval type t) '(boolean integer number string)))
(error "Macro defpacustom: missing :type keyword or wrong :type value"))
;; Error in case a defpacustom is repeated.
@@ -212,21 +212,23 @@ Usage: (defpgdefault SYM VALUE)"
(eval
`(defpgcustom ,name ,val
,@newargs
- :set 'proof-set-value
- :group (quote ,proof-assistant-cusgrp)))
+ :set #'proof-set-value
+ :group (quote ,proof-assistant-cusgrp))
+ t)
(cond
(evalform
(eval
`(defpgfun ,name ()
- ,evalform)))
+ ,evalform)
+ t))
(setting
(eval
`(defpgfun ,name ()
(proof-assistant-invisible-command-ifposs
- (proof-assistant-settings-cmd (quote ,name)))))))
- (setq proof-assistant-settings
- (cons (list name setting (eval type) descr)
- proof-assistant-settings))))
+ (proof-assistant-settings-cmd (quote ,name))))
+ t)))
+ (push (list name setting (eval type t) descr)
+ proof-assistant-settings)))
;;;###autoload
(defmacro defpacustom (name val &rest args)
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 6651e27..2d3a095 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -101,7 +101,7 @@ Called from `proof-done-advancing' when a save is processed
and
;; one depends on; update their list of dependents,
;; and return resulting list paired up with names.
(depspans
- (apply 'append
+ (apply #'append
(span-mapcar-spans
(lambda (depspan)
(let ((dname (span-property depspan 'name)))
@@ -144,15 +144,15 @@ specific entries."
(list
"-------------"
(proof-dep-make-submenu "Local Dependency..."
- (lambda (namespan) (car namespan))
- 'proof-goto-dependency
+ #'car
+ #'proof-goto-dependency
(span-property span
'dependencies-within-file))
(proof-make-highlight-depts-menu "Highlight Dependencies"
'proof-highlight-depcs
span 'dependencies-within-file)
(proof-dep-make-submenu "Local Dependents..."
- (lambda (namepos) (car namepos))
- 'proof-goto-dependency
+ #'car
+ #'proof-goto-dependency
(span-property span 'dependents))
(proof-make-highlight-depts-menu "Highlight Dependents"
'proof-highlight-depts
@@ -184,9 +184,9 @@ specific entries."
(cdr nestedtop))
(mapcar (lambda (sm)
(proof-dep-make-submenu (car sm)
- 'car
- 'proof-show-dependency
- (mapcar 'list (cdr sm))))
+ #'car
+ #'proof-show-dependency
+ (mapcar #'list (cdr sm))))
(car nestedtop)))))
(vector menuname nil nil))))
@@ -214,9 +214,10 @@ If LIST is empty, return a disabled menu item with NAME.
NAMEFN is applied to each element of LIST to make the names."
(if list
(cons name
- (mapcar `(lambda (l)
- (vector (,namefn l)
- (cons (quote ,appfn) l) t)) list))
+ (mapcar (lambda (l)
+ (vector (funcall namefn l)
+ (cons appfn l) t))
+ list))
(vector name nil nil)))
(defun proof-make-highlight-depts-menu (name fn span prop)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0c4a980..639d51d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -86,6 +86,7 @@ If ASSISTANT-NAME is omitted, look up in
`proof-assistant-table'."
(cus-internals (intern (concat cusgrp-rt "-config")))
(elisp-dir sname) ; NB: dirname same as symbol name!
(loadpath-elt (concat proof-home-directory elisp-dir "/")))
+ ;; FIXME: Yuck!!
(eval `(progn
;; Make a customization group for this assistant
(defgroup ,cusgrp nil
@@ -116,11 +117,12 @@ If ASSISTANT-NAME is omitted, look up in
`proof-assistant-table'."
;; Extend the load path if necessary
(proof-add-to-load-path ,loadpath-elt)
;; Run hooks for late initialisation
- (run-hooks 'proof-ready-for-assistant-hook))))))
+ (run-hooks 'proof-ready-for-assistant-hook))
+ t))))
(defalias 'proof-active-buffer-fake-minor-mode
- 'proof-toggle-active-scripting)
+ #'proof-toggle-active-scripting)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -601,8 +603,7 @@ It is recorded in the span with the 'rawname property."
(rawname name)
(name (or name id))
(idiom (symbol-name idiomsym))
- (delfn `(lambda () (pg-remove-element
- (quote ,idiomsym) (quote ,idsym))))
+ (delfn (lambda () (pg-remove-element idiomsym idsym)))
(elts (cdr-safe (assq idiomsym pg-script-portions))))
(unless elts
(setq pg-script-portions
@@ -741,7 +742,7 @@ Each span has a 'type property, one of:
(defvar pg-span-context-menu-keymap
(let ((map (make-sparse-keymap
"Keymap for context-sensitive menus on spans")))
- (define-key map [down-mouse-3] 'pg-span-context-menu)
+ (define-key map [down-mouse-3] #'pg-span-context-menu)
map)
"Keymap for the span context menu.")
@@ -1465,8 +1466,7 @@ that is not yet documented here, this function
(+ (length comment-start) (span-start span))
(- (span-end span)
(max 1 (length comment-end)))))
- (id (proof-next-element-id 'comment))
- str)
+ (id (proof-next-element-id 'comment)))
(pg-add-element 'comment id bodyspan)
(span-set-property span 'id (intern id))
(span-set-property span 'idiom 'comment)
@@ -2027,7 +2027,7 @@ start is found inside a proof."
(while vanillas
(setq item (car vanillas))
;; cdr vanillas is at the end of the loop
- (setq cmd (mapconcat 'identity (nth 1 item) " "))
+ (setq cmd (mapconcat #'identity (nth 1 item) " "))
(if inside-proof
(progn
(if (string-match proof-script-proof-start-regexp cmd)
@@ -2790,9 +2790,9 @@ finish setup which depends on specific proof assistant
configuration."
;; This key-binding was disabled following a request in PG issue #160.
;; (define-key proof-mode-map
;; (vconcat [(control c)] (vector (aref proof-terminal-string 0)))
-;; 'proof-electric-terminator-toggle)
+;; #'proof-electric-terminator-toggle)
(define-key proof-mode-map (vector (aref proof-terminal-string 0))
- 'proof-electric-terminator)))
+ #'proof-electric-terminator)))
;; Toolbar, main menu (loads proof-toolbar,setting p.-toolbar-scripting-menu)
(proof-toolbar-setup)
@@ -2800,8 +2800,6 @@ finish setup which depends on specific proof assistant
configuration."
;; Menus: the Proof-General and the specific menu
(proof-menu-define-main)
(proof-menu-define-specific)
- (easy-menu-add proof-mode-menu proof-mode-map)
- (easy-menu-add proof-assistant-menu proof-mode-map)
;; Define parsing functions
(proof-setup-parsing-mechanism)
diff --git a/generic/proof-site.el b/generic/proof-site.el
index b149b7f..74bdaea 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -189,7 +189,7 @@ proof-site.el couldn't know where it was executed from.")
(list dne)
nil)))
proof-assistant-table-default))
- "*Proof General's table of supported proof assistants.
+ "Proof General's table of supported proof assistants.
This is copied from `proof-assistant-table-default' at load time,
removing any entries that do not have a corresponding directory
under `proof-home-directory'.
@@ -220,11 +220,12 @@ variable `proof-home-directory'."
(defcustom proof-assistants nil
(concat
- "*Choice of proof assistants to use with Proof General.
-A list of symbols chosen from:"
- (apply 'concat (mapcar (lambda (astnt)
- (concat " '" (symbol-name (car astnt))))
- proof-assistant-table))
+ "Choice of proof assistants to use with Proof General.
+A list of symbols chosen from: "
+ (mapconcat (lambda (astnt)
+ (concat "`" (symbol-name (car astnt)) "'"))
+ proof-assistant-table
+ " ")
".\nIf nil, the default will be ALL available proof assistants.
Each proof assistant defines its own instance of Proof General,
@@ -247,9 +248,10 @@ Note: to change proof assistant, you must start a new
Emacs session.")
:group 'proof-general)
(defvar proof-general-configured-provers
- (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS")
"")))
+ (or (mapcar #'intern (split-string
+ (or (getenv "PROOFGENERAL_ASSISTANTS") "")))
proof-assistants
- (mapcar (lambda (astnt) (car astnt)) proof-assistant-table))
+ (mapcar #'car proof-assistant-table))
"A list of the configured proof assistants.
Set on startup to contents of environment variable PROOFGENERAL_ASSISTANTS,
the Lisp variable `proof-assistants', or the contents of
`proof-assistant-table'.")
@@ -279,6 +281,8 @@ the Lisp variable `proof-assistants', or the contents of
`proof-assistant-table'
;; Stub to initialize and load specific code.
(mode-stub
+ ;; FIXME: Make it a closure with (:documentation EXP)
+ ;; once we don't need compatibility with Emacs<25.
`(lambda ()
,(concat
"Major mode for editing scripts for proof assistant "
@@ -321,7 +325,7 @@ the Lisp variable `proof-assistants', or the contents of
`proof-assistant-table'
(defun proof-chose-prover (prompt)
(completing-read prompt
- (mapcar 'symbol-name
+ (mapcar #'symbol-name
proof-general-configured-provers)))
(defun proofgeneral (prover)
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index bb8b5c0..da5402a 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -1,9 +1,9 @@
-;;; proof-splash.el --- Splash welcome screen for Proof General
+;;; proof-splash.el --- Splash welcome screen for Proof General -*-
lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -109,8 +109,8 @@ If it is nil, a new line is inserted."
(set-buffer-modified-p nil)
(setq buffer-read-only t))
-(define-key proof-splash-mode-map "q" 'bury-buffer)
-(define-key proof-splash-mode-map [mouse-3] 'bury-buffer)
+(define-key proof-splash-mode-map "q" #'bury-buffer)
+(define-key proof-splash-mode-map [mouse-3] #'bury-buffer)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -157,7 +157,7 @@ Borrowed from startup-center-spaces."
;; Symptom is ProofGeneral mode instead of the native script mode.
;;
-(defun proof-splash-remove-screen (&optional nothing)
+(defun proof-splash-remove-screen (&optional _nothing)
"Remove splash screen and restore window config."
(let ((splashbuf (get-buffer proof-splash-welcome)))
(proof-splash-unset-frame-titles)
@@ -192,8 +192,8 @@ Borrowed from startup-center-spaces."
"Insert splash buffer contents into current buffer."
(let*
((splash-contents (append
- (eval proof-splash-contents)
- (eval proof-splash-startup-msg)))
+ (eval proof-splash-contents t)
+ (eval proof-splash-startup-msg t)))
s)
(setq buffer-read-only nil)
(erase-buffer)
@@ -258,13 +258,13 @@ binding to remove this buffer."
(setq proof-splash-timeout-conf
(cons
(add-timeout proof-splash-time
- 'proof-splash-remove-screen nil)
+ #'proof-splash-remove-screen nil)
savedwincnf))
- (add-hook 'proof-mode-hook 'proof-splash-timeout-waiter))))
+ (add-hook 'proof-mode-hook #'proof-splash-timeout-waiter))))
(setq proof-splash-seen t)))
-(defalias 'pg-about 'proof-splash-display-screen)
+(defalias 'pg-about #'proof-splash-display-screen)
;;;###autoload
(defun proof-splash-message ()
@@ -279,9 +279,8 @@ binding to remove this buffer."
;; otherwise it can have undesired interference.
(run-with-timer
0 nil
- `(lambda ()
- (proof-splash-display-screen
- ,(not (called-interactively-p 'any))))))
+ (let ((nci (not (called-interactively-p 'any))))
+ (lambda () (proof-splash-display-screen nci)))))
;; Otherwise, a message
(message "Welcome to %s Proof General!" proof-assistant))
(setq proof-splash-seen t)))
@@ -297,7 +296,7 @@ binding to remove this buffer."
(if (input-pending-p)
(setq unread-command-events
(cons (next-command-event) unread-command-events))))
- (remove-hook 'proof-mode-hook 'proof-splash-timeout-waiter))
+ (remove-hook 'proof-mode-hook #'proof-splash-timeout-waiter))
(defvar proof-splash-old-frame-title-format nil)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 1a01147..8ea26cc 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -1,9 +1,9 @@
-;;; proof-tree.el --- Proof General prooftree communication.
+;;; proof-tree.el --- Proof General prooftree communication. -*-
lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -467,7 +467,7 @@ from `proof-tree-process-filter' when more output arrives.")
;; there yet
;; need to try again later
(setq proof-tree-filter-continuation
- `(lambda () (proof-tree-insert-script ,data)))))
+ (lambda () (proof-tree-insert-script data)))))
(display-warning
'(proof-general proof-tree)
"Prooftree sent an invalid data length for insert-command"
@@ -490,7 +490,7 @@ newly arrived output."
(if moving (goto-char (point-max))))))
-(defun proof-tree-process-filter (proc string)
+(defun proof-tree-process-filter (_proc string)
"Output filter for prooftree.
Records the output in the prooftree process buffer and checks for
callback function requests. Such callback functions might fail
@@ -550,7 +550,7 @@ everything is processed, the marker is deleted and
;; Process creation
;;
-(defun proof-tree-process-sentinel (proc event)
+(defun proof-tree-process-sentinel (_proc event)
"Sentinel for prooftee.
Runs on process status changes and cleans up when prooftree dies."
(proof-tree-insert-output (concat "\nsubprocess status change: " event) t)
@@ -579,14 +579,14 @@ variables."
;; now start the new process
(proof-tree-insert-output "\nStart new prooftree process\n\n" t)
(setq proof-tree-process
- (apply 'start-process
+ (apply #'start-process
proof-tree-process-name
proof-tree-process-buffer
proof-tree-program
proof-tree-arguments))
(set-process-coding-system proof-tree-process 'utf-8-unix 'utf-8-unix)
- (set-process-filter proof-tree-process 'proof-tree-process-filter)
- (set-process-sentinel proof-tree-process 'proof-tree-process-sentinel)
+ (set-process-filter proof-tree-process #'proof-tree-process-filter)
+ (set-process-sentinel proof-tree-process #'proof-tree-process-sentinel)
(set-process-query-on-exit-flag proof-tree-process nil)
;; other initializations
(setq proof-tree-sequent-hash (make-hash-table :test 'equal)
@@ -627,7 +627,7 @@ DATA as data sections to Prooftree."
(format "second line %03d\n%s\n%s%s"
(1+ second-line-len)
second-line
- (mapconcat 'identity data "\n")
+ (mapconcat #'identity data "\n")
(if data "\n" "")))))
(defun proof-tree-send-configure ()
@@ -645,7 +645,7 @@ DATA as data sections to Prooftree."
"Send the current goal state to prooftree."
;; (message "PTSGS id %s sequent %s ex-info %s"
;; current-sequent-id current-sequent-text existential-info)
- (let* ((add-id-string (mapconcat 'identity additional-sequent-ids " "))
+ (let* ((add-id-string (mapconcat #'identity additional-sequent-ids " "))
(second-line
(format
(concat "current-goals state %d current-sequent %s %s %s "
@@ -819,7 +819,7 @@ lambda expressions that you can put into
`proof-action-list'."
(defun proof-tree-make-show-goal-callback (state)
"Create the callback for display-goal commands."
- `(lambda (span) (proof-tree-show-goal-callback ,state)))
+ (lambda (_span) (proof-tree-show-goal-callback state)))
(defun proof-tree-urgent-action (flags)
"Handle urgent points before the next item is sent to the proof assistant.
@@ -1054,8 +1054,8 @@ The delayed output of the navigation command is in the
region
(defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info)
"Display current goal in prooftree unless CMD should be ignored."
;; (message "PTHPC")
- (let ((proof-state (car proof-info))
- (cmd-string (mapconcat 'identity cmd " ")))
+ (let (;; (proof-state (car proof-info))
+ (cmd-string (mapconcat #'identity cmd " ")))
(unless (and proof-tree-ignored-commands-regexp
(proof-string-match proof-tree-ignored-commands-regexp
cmd-string))
@@ -1140,7 +1140,7 @@ The delayed output is in the region
sequent-text)))))))
-(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span)
+(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags _span)
"Process delayed output for prooftree.
This function is the main entry point of the Proof General
prooftree support. It examines the delayed output in order to
@@ -1205,7 +1205,7 @@ the flags and SPAN is the span."
(if (and proof-tree-configured (proof-tree-is-running))
(proof-tree-send-undo 0)))
-(add-hook 'proof-deactivate-scripting-hook 'proof-tree-leave-buffer)
+(add-hook 'proof-deactivate-scripting-hook #'proof-tree-leave-buffer)
;;
