Thanks a lot Stefan,
I am very worried about the async branch. Its state is not usable at
this moment (lots of bugs) imho and we have nobody to maintain and fix
it currently.
Do we really want to be compatible with ubuntu 14.04? I mean there are
18.04 and now 20.04 out there...
P.
Le jeu. 29 nov. 2018 à 03:19, Stefan Monnier
<monn...@iro.umontreal.ca> a écrit :
>
> > Yes, exactly. `master` is still the mainline branch to integrate new PRs
> > while the nextgen implementation available in `async` is still in alpha
> > phase.
>
> OK, good.
>
> > We'd specifically want to keep support of Emacs 24.3 for the moment
> > because this is still the version of the emacs24 package distributed
> > in Ubuntu 14.04 LTS:
>
> OK, thanks.
>
> Find below a first patch. I'd be interested to try out the `async`
> branch (and maybe help keep it up-to-date with `master`), but I can't
> get it to work (with Emacs and Coq from Debian stable). I understand
> it's work-in-progress, but is there a setup that's known to work, so
> I can try and detect regressions?
>
>
> Stefan
>
>
> 2018-11-28 Stefan Monnier <monn...@iro.umontreal.ca>
>
> Move `defvar`s used to silence warnings outside of eval-when-compile.
> Make sure they don't actually give a value to the var.
>
> * pg-init.el: Simplify.
> Use (if t ...) to avoid running `require` at compile-time.
> Don't add subdirs to load-path here since this code is never used.
> (pg-init--script-full-path, pg-init--pg-root):
> Inline their definition into their sole user.
>
> * generic/proof-utils.el (proof-resize-window-tofit):
> Inline definitions of window-leftmost-p and window-rightmost-p previously
> in proof-compat.el.
>
> * lib/proof-compat.el (proof-running-on-win32): Remove, not used.
> (mac-key-mode): Remove, there's no carbon-emacs-package-version in
> Emacs≥24.3.
> (pg-custom-undeclare-variable): Use dolist.
> (save-selected-frame): Remove, save-selected-window also saves&restores
> the selected frame at the same time. Update all users (which already
> used save-selected-window around it).
> (window-leftmost-p, window-rightmost-p, window-bottom-p)
> (find-coding-system): Remove, unused.
>
> * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar
> it to a dummy value and...
> (hol-light): ...check its existence before using it instead.
>
> * coq/coq.el (coq-may-use-prettify): Simplify initialization.
>
>
>
> diff --git a/.gitignore b/.gitignore
> index 9cd6d703..2039757e 100644
> --- a/.gitignore
> +++ b/.gitignore
> @@ -2,5 +2,6 @@
> nohup.out
> TAGS
> ChangeLog
> +proof-general-autoloads.el
> *.elc
> *~
> diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
> index 97ea6ec6..9dca0082 100644
> --- a/coq/coq-compile-common.el
> +++ b/coq/coq-compile-common.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
> @@ -26,10 +26,9 @@
> (require 'coq-system)
> (require 'compile)
>
> -(eval-when-compile
> - ;;(defvar coq-pre-v85 nil)
> - (defvar coq-confirm-external-compilation); defpacustom
> - (defvar coq-compile-parallel-in-background)) ; defpacustom
> +;;(defvar coq-pre-v85 nil)
> +(defvar coq-confirm-external-compilation); defpacustom
> +(defvar coq-compile-parallel-in-background) ; defpacustom
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> diff --git a/coq/coq-indent.el b/coq/coq-indent.el
> index 6e8ba013..af780251 100644
> --- a/coq/coq-indent.el
> +++ b/coq/coq-indent.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
> @@ -33,8 +33,7 @@
> ; ,@body
> ; (message "%.06f" (float-time (time-since time)))))
>
> -(eval-when-compile
> - (defvar coq-script-indent))
> +(defvar coq-script-indent)
>
> (defconst coq-any-command-regexp
> (proof-regexp-alt-list coq-keywords))
> diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
> index b8c5d7e3..f172adbe 100644
> --- a/coq/coq-local-vars.el
> +++ b/coq/coq-local-vars.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
> @@ -22,9 +22,8 @@
> (eval-when-compile
> (require 'cl))
>
> -(eval-when-compile
> - (defvar coq-prog-name)
> - (defvar coq-load-path))
> +(defvar coq-prog-name)
> +(defvar coq-load-path)
>
>
> (defconst coq-local-vars-doc nil
> diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
> index e3daebcd..b03fedaa 100644
> --- a/coq/coq-par-compile.el
> +++ b/coq/coq-par-compile.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
> @@ -37,8 +37,7 @@
> (eval-when-compile
> (require 'proof-compat))
>
> -(eval-when-compile
> - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook
> +(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
>
> (require 'coq-compile-common)
>
> diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
> index 5875908c..74327b53 100644
> --- a/coq/coq-seq-compile.el
> +++ b/coq/coq-seq-compile.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
> @@ -27,8 +27,7 @@
> (eval-when-compile
> (require 'proof-compat))
>
> -(eval-when-compile
> - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook
> +(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
>
> (require 'coq-compile-common)
>
> diff --git a/coq/coq-system.el b/coq/coq-system.el
> index 68d036f1..bb1c28f0 100644
> --- a/coq/coq-system.el
> +++ b/coq/coq-system.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
> @@ -29,9 +29,8 @@
> (require 'cl)
> (require 'proof-compat))
>
> -(eval-when-compile
> - (defvar coq-prog-args)
> - (defvar coq-debug))
> +(defvar coq-prog-args)
> +(defvar coq-debug)
>
> ;; Arbitrary arguments can already be passed through _CoqProject.
> ;; However this is not true for all assistants, so we don't modify the
> diff --git a/coq/coq.el b/coq/coq.el
> index 3376f7f3..6b1494a9 100644
> --- a/coq/coq.el
> +++ b/coq/coq.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
> @@ -28,21 +28,20 @@
> (require 'span)
> (require 'outline)
> (require 'newcomment)
> - (require 'etags)
> - (unless (proof-try-require 'smie)
> - (defvar smie-indent-basic)
> - (defvar smie-rules-function))
> - (defvar proof-info) ; dynamic scope in proof-tree-urgent-action
> - (defvar action) ; dynamic scope in coq-insert-as stuff
> - (defvar string) ; dynamic scope in coq-insert-as stuff
> - (defvar old-proof-marker)
> - (defvar coq-keymap)
> - (defvar coq-one-command-per-line)
> - (defvar coq-auto-insert-as) ; defpacustom
> - (defvar coq-time-commands) ; defpacustom
> - (defvar coq-use-project-file) ; defpacustom
> - (defvar coq-use-editing-holes) ; defpacustom
> - (defvar coq-hide-additional-subgoals))
> + (require 'etags))
> +(defvar smie-indent-basic)
> +(defvar smie-rules-function)
> +(defvar proof-info) ; dynamic scope in proof-tree-urgent-action
> +(defvar action) ; dynamic scope in coq-insert-as stuff
> +(defvar string) ; dynamic scope in coq-insert-as stuff
> +(defvar old-proof-marker)
> +(defvar coq-keymap)
> +(defvar coq-one-command-per-line)
> +(defvar coq-auto-insert-as) ; defpacustom
> +(defvar coq-time-commands) ; defpacustom
> +(defvar coq-use-project-file) ; defpacustom
> +(defvar coq-use-editing-holes) ; defpacustom
> +(defvar coq-hide-additional-subgoals)
>
> (require 'proof)
> (require 'coq-system) ; load path, option, project file
> etc.
> @@ -66,11 +65,8 @@
>
> ;; prettify is in emacs > 24.4
> ;; FIXME: this should probably be done like for smie above.
> -(defvar coq-may-use-prettify nil) ; may become t below
> -(eval-when-compile
> - (if (fboundp 'prettify-symbols-mode)
> - (defvar coq-may-use-prettify t)
> - (defvar prettify-symbols-alist nil)))
> +(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
> +(defvar prettify-symbols-alist)
>
>
> ;; ----- coq-shell configuration options
> @@ -911,22 +907,21 @@ This is mapped to control/shift mouse-1, unless
> coq-remap-mouse-1
> is nil (t by default)."
> (interactive "e")
> (save-selected-window
> - (save-selected-frame
> - (save-excursion
> - (mouse-set-point event)
> - (let* ((id (coq-id-at-point))
> - (notat (coq-notation-at-position (point)))
> - (modifs (event-modifiers event))
> - (shft (member 'shift modifs))
> - (ctrl (member 'control modifs))
> - (cmd (when (or id notat)
> - (if (and ctrl shft) (if id "Check" "Locate")
> - (if shft (if id "About" "Locate")
> - (if ctrl (if id "Print" "Locate")))))))
> - (proof-shell-invisible-command
> - (format (concat cmd " %s . ")
> - ;; Notation need to be surrounded by ""
> - (if id id (concat "\"" notat "\"")))))))))
> + (save-excursion
> + (mouse-set-point event)
> + (let* ((id (coq-id-at-point))
> + (notat (coq-notation-at-position (point)))
> + (modifs (event-modifiers event))
> + (shft (member 'shift modifs))
> + (ctrl (member 'control modifs))
> + (cmd (when (or id notat)
> + (if (and ctrl shft) (if id "Check" "Locate")
> + (if shft (if id "About" "Locate")
> + (if ctrl (if id "Print" "Locate")))))))
> + (proof-shell-invisible-command
> + (format (concat cmd " %s . ")
> + ;; Notation need to be surrounded by ""
> + (if id id (concat "\"" notat "\""))))))))
>
> (defun coq-guess-or-ask-for-string (s &optional dontguess)
> "Asks for a coq identifier with message S.
> @@ -1211,8 +1206,7 @@ Printing All set."
> (coq-ask-do-show-all "Show goal number" "Show" t))
>
> ;; Check
> -(eval-when-compile
> - (defvar coq-auto-adapt-printing-width)); defpacustom
> +(defvar coq-auto-adapt-printing-width); defpacustom
>
> ;; Since Printing Width is a synchronized option in coq (?) it is retored
> ;; silently to a previous value when retracting. So we reset the stored width
> diff --git a/generic/pg-goals.el b/generic/pg-goals.el
> index baab5561..124965e8 100644
> --- a/generic/pg-goals.el
> +++ b/generic/pg-goals.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
> @@ -20,9 +20,9 @@
> (eval-when-compile
> (require 'easymenu) ; easy-menu-add, etc
> (require 'cl) ; incf
> - (require 'span) ; span-*
> - (defvar proof-goals-mode-menu) ; defined by macro below
> - (defvar proof-assistant-menu)) ; defined by macro in proof-menu
> + (require 'span)) ; span-*
> +(defvar proof-goals-mode-menu) ; defined by macro below
> +(defvar proof-assistant-menu) ; defined by macro in proof-menu
>
> (require 'pg-assoc)
>
> diff --git a/generic/pg-response.el b/generic/pg-response.el
> index 43e0e279..650e83a0 100644
> --- a/generic/pg-response.el
> +++ b/generic/pg-response.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
> @@ -24,9 +24,9 @@
>
> (eval-when-compile
> (require 'easymenu) ; easy-menu-add
> - (require 'proof-utils) ; deflocal, proof-eval-when-ready-for-assistant
> - (defvar proof-response-mode-menu nil)
> - (defvar proof-assistant-menu nil))
> + (require 'proof-utils)) ; deflocal, proof-eval-when-ready-for-assistant
> +(defvar proof-response-mode-menu)
> +(defvar proof-assistant-menu)
>
> (require 'pg-assoc)
> (require 'span)
> diff --git a/generic/pg-user.el b/generic/pg-user.el
> index 126901cb..5a5d6d13 100644
> --- a/generic/pg-user.el
> +++ b/generic/pg-user.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
> @@ -863,10 +863,9 @@ The function `substitute-command-keys' is called on the
> argument."
> (interactive "e")
> (if proof-query-identifier-command
> (save-selected-window
> - (save-selected-frame
> - (save-excursion
> - (mouse-set-point event)
> - (pg-identifier-near-point-query))))))
> + (save-excursion
> + (mouse-set-point event)
> + (pg-identifier-near-point-query)))))
>
> ;;;###autoload
> (defun pg-identifier-near-point-query ()
> diff --git a/generic/proof-menu.el b/generic/proof-menu.el
> index fc18d504..027d0c7d 100644
> --- a/generic/proof-menu.el
> +++ b/generic/proof-menu.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
> @@ -19,9 +19,8 @@
> ;;; Code:
> (require 'cl) ; mapcan
>
> -(eval-when-compile
> - (defvar proof-assistant-menu) ; defined by macro in
> proof-menu-define-specific
> - (defvar proof-mode-map))
> +(defvar proof-assistant-menu) ; defined by macro in
> proof-menu-define-specific
> +(defvar proof-mode-map)
>
> (require 'proof-utils) ; proof-deftoggle,
> proof-eval-when-ready-for-assistant
> (require 'proof-useropts)
> diff --git a/generic/proof-script.el b/generic/proof-script.el
> index c938dfad..9c5c06a4 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, 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,9 +30,9 @@
> (require 'proof-syntax) ; utils for manipulating
> syntax
>
> (eval-when-compile
> - (require 'easymenu)
> - (defvar proof-mode-menu nil)
> - (defvar proof-assistant-menu nil))
> + (require 'easymenu))
> +(defvar proof-mode-menu)
> +(defvar proof-assistant-menu)
>
> (declare-function proof-shell-strip-output-markup "proof-shell"
> (string &optional push))
> diff --git a/generic/proof-shell.el b/generic/proof-shell.el
> index b5bbcd9f..51d10c2c 100644
> --- a/generic/proof-shell.el
> +++ b/generic/proof-shell.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
> @@ -34,9 +34,8 @@
> (declare-function proof-tree-urgent-action "proof-tree" (flags))
> (declare-function proof-tree-handle-delayed-output "proof-tree"
> (old-proof-marker cmd flags span))
> -(eval-when-compile
> - ;; without the nil initialization the compiler still warns about this
> variable
> - (defvar proof-tree-external-display nil))
> +;; without the nil initialization the compiler still warns about this
> variable
> +(defvar proof-tree-external-display)
>
> (require 'scomint)
> (require 'pg-response)
> @@ -454,8 +453,7 @@ process command."
> ;; Call multiple-frames-enable in case we need to fire up
> ;; new frames (NB: sets specifiers to remove modeline)
> (save-selected-window
> - (save-selected-frame
> - (proof-multiple-frames-enable)))))
> + (proof-multiple-frames-enable))))
>
> (message "Starting %s process... done." proc))))
>
> diff --git a/generic/proof-site.el b/generic/proof-site.el
> index e339d022..fd48002f 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, 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
> @@ -169,8 +169,7 @@ You can use customize to set this variable."
> (require 'pg-vars)
> (require 'proof-autoloads)
>
> -(eval-when-compile
> - (defvar Info-dir-contents))
> +(defvar Info-dir-contents)
>
> ;; Add the info directory to the Info path
> (if (file-exists-p proof-info-directory) ; for safety
> diff --git a/generic/proof-utils.el b/generic/proof-utils.el
> index b4e7e0d1..a2c29824 100644
> --- a/generic/proof-utils.el
> +++ b/generic/proof-utils.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
> @@ -40,7 +40,7 @@
>
> (if (or (not (boundp 'emacs-major-version))
> (< emacs-major-version 23)
> - (string-match "XEmacs" emacs-version))
> + (featurep 'xemacs))
> (error "Proof General is not compatible with Emacs %s" emacs-version))
>
> (unless (equal pg-compiled-for (pg-emacs-version-cookie))
> @@ -399,8 +399,9 @@ or if the window is the only window of its frame."
> (select-window window))))
> ;; the window is the full width, right?
> ;; [if not, we may be in horiz-split scheme, problematic]
> - (not (window-leftmost-p window))
> - (not (window-rightmost-p window)))
> + (not (zerop (car (window-edges window)))) ;not leftmost
> + (not (>= (nth 2 (window-edges window)) ;not rightmost
> + (frame-width (window-frame window)))))
> ;; OK, we're not going to adjust the height here. Moreover,
> ;; we'll make sure the height can be changed elsewhere.
> (setq window-size-fixed nil)
> diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
> index 2b4f3989..808e04a9 100644
> --- a/hol-light/hol-light.el
> +++ b/hol-light/hol-light.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
> @@ -22,12 +22,10 @@
> (require 'proof-easy-config) ; easy configure mechanism
> (require 'proof-syntax) ; functions for making regexps
>
> -(or (proof-try-require 'caml-font) ; use OCaml Emacs mode syntax
> - (defvar caml-font-lock-keywords nil)) ;
> +(proof-try-require 'caml-font) ; use OCaml Emacs mode syntax
>
> (eval-when-compile
> - (require 'proof-tree)
> - (defvar caml-font-lock-keywords nil))
> + (require 'proof-tree))
>
> (defcustom hol-light-home
> (or (getenv "HOLLIGHT_HOME")
> @@ -317,7 +315,7 @@ You need to restart Emacs if you change this setting."
>
> proof-script-font-lock-keywords
> (append
> - caml-font-lock-keywords
> + (bound-and-true-p caml-font-lock-keywords)
> (list
> (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face)
> (cons (proof-ids-to-regexp hol-light-tactics) 'proof-tactics-name-face)
> diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
> index e399474b..0b61aab0 100644
> --- a/isar/isabelle-system.el
> +++ b/isar/isabelle-system.el
> @@ -1,6 +1,7 @@
> ;; isabelle-system.el --- Interface with Isabelle system
> ;;
> ;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall.
> +;; Copyright (C) 2018 Free Software Foundation, Inc.
> ;;
> ;; Author: David Aspinall <d...@dcs.ed.ac.uk>
> ;; Maintainer: Proof General maintainer <proof...@dcs.ed.ac.uk>
> @@ -20,8 +21,8 @@
> (require 'scomint)
> (require 'proof-site)
> (require 'proof-menu)
> - (require 'proof-syntax)
> - (defvar proof-assistant-menu))
> + (require 'proof-syntax))
> +(defvar proof-assistant-menu)
>
> (declare-function mapcan "cl-extra") ; spurious bytecomp warning
>
> diff --git a/isar/isar.el b/isar/isar.el
> index bb755d4f..917f8f6a 100644
> --- a/isar/isar.el
> +++ b/isar/isar.el
> @@ -1,6 +1,7 @@
> ;; isar.el --- Major mode for Isabelle/Isar proof assistant
> ;;
> ;; Copyright (C) 1994-2010 LFCS Edinburgh.
> +;; Copyright (C) 2018 Free Software Foundation, Inc.
> ;;
> ;; License: GPL (GNU GENERAL PUBLIC LICENSE)
> ;;
> @@ -24,10 +25,10 @@
> (require 'proof-syntax)
> (require 'pg-goals)
> (require 'pg-vars)
> - (require 'outline)
> - (defvar comment-quote-nested)
> - (defvar isar-use-find-theorems-form)
> - (defvar isar-use-linear-undo))
> + (require 'outline))
> +(defvar comment-quote-nested)
> +(defvar isar-use-find-theorems-form)
> +(defvar isar-use-linear-undo)
>
> (require 'proof)
> (require 'isabelle-system) ; system code
> diff --git a/lib/proof-compat.el b/lib/proof-compat.el
> index abbdb465..25c029c6 100644
> --- a/lib/proof-compat.el
> +++ b/lib/proof-compat.el
> @@ -1,9 +1,9 @@
> -;;; proof-compat.el --- Operating system and Emacs version compatibility
> +;;; proof-compat.el --- Operating system and Emacs version compatibility
> -*- 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-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
> @@ -28,31 +28,10 @@
>
> ;;; Code:
>
> -(require 'easymenu)
> (require 'cl)
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;;
> -;;; Architecture flags
> -;;;
> -
> -;; can use eval-and-compile to allow optimisation, but that would
> -;; require recompilation for Windows
> -(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin))
> - "Non-nil if Proof General is running on a windows variant system.")
> -
> -
> -;; Workaround a small bug in Carbon Emacs Winter 2008 (at least)
> -;; Menu presses query this variable, but it's not bound unless
> -;; mode engaged. Not noticeable in normal use, but it is as soon
> -;; as debug-on-error is engaged.
> -(with-no-warnings
> - (if (and (boundp 'carbon-emacs-package-version)
> - (not (boundp 'mac-key-mode)))
> - (setq mac-key-mode nil)))
> -
> -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> -;;;
> ;;; Modifications and adjustments
> ;;;
>
> @@ -64,8 +43,8 @@
> Done by removing all properties mentioned by custom library.
> The symbol itself is left defined, in case it has been changed
> in the current Emacs session."
> - (mapc (lambda (prop) (remprop symbol prop))
> - '(default
> + (dolist (prop
> + '(default
> standard-value
> force-value
> variable-comment
> @@ -83,49 +62,8 @@ in the current Emacs session."
> custom-version
> saved-value
> theme-value
> - theme-face)))
> -
> -
> -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> -;;;
> -;;; GNU Emacs compatibility with XEmacs
> -;;;
> -
> -(unless (fboundp 'save-selected-frame)
> -(defmacro save-selected-frame (&rest body)
> - "Execute forms in BODY, then restore the selected frame.
> -The value returned is the value of the last form in BODY."
> - (let ((old-frame (gensym "ssf")))
> - `(let ((,old-frame (selected-frame)))
> - (unwind-protect
> - (progn ,@body)
> - (select-frame ,old-frame))))))
> -
> -;; These functions are used in the intricate logic around
> -;; shrink-to-fit.
> -
> -;; window-leftmost-p, window-rightmost-p: my implementations
> -(or (fboundp 'window-leftmost-p)
> - (defun window-leftmost-p (window)
> - (zerop (car (window-edges window)))))
> -
> -(or (fboundp 'window-rightmost-p)
> - (defun window-rightmost-p (window)
> - (>= (nth 2 (window-edges window))
> - (frame-width (window-frame window)))))
> -
> -(or (fboundp 'window-bottom-p)
> - (defun window-bottom-p (window)
> - (>= (nth 3 (window-edges window))
> - (frame-height (window-frame window)))))
> -
> -;; find-coding-system emulation for GNU Emacs
> -(unless (fboundp 'find-coding-system)
> - (defun find-coding-system (name)
> - "Retrieve the coding system of the given name, or nil if non-such."
> - (condition-case nil
> - (check-coding-system name)
> - (error nil))))
> + theme-face))
> + (remprop symbol prop)))
>
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> @@ -137,9 +75,9 @@ The value returned is the value of the last form in BODY."
> ;; makes every suffix be added as a completion!
>
> (eval-after-load "completion"
> -'(defun completion-before-command ()
> - (if (and (symbolp this-command) (get this-command 'completion-function))
> - (funcall (get this-command 'completion-function)))))
> + '(defun completion-before-command ()
> + (if (and (symbolp this-command) (get this-command 'completion-function))
> + (funcall (get this-command 'completion-function)))))
>
> (provide 'proof-compat)
> ;;; proof-compat.el ends here
> diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
> index f5462ba6..09a61b27 100644
> --- a/obsolete/plastic/plastic.el
> +++ b/obsolete/plastic/plastic.el
> @@ -1,5 +1,7 @@
> ;; plastic.el - Major mode for Plastic proof assistant
> ;;
> +;; Portions © Copyright 2018 Free Software Foundation, Inc.
> +;;
> ;; Author: Paul Callaghan <p.c.callag...@durham.ac.uk>
> ;;
> ;; $Id$
> @@ -15,8 +17,8 @@
> (require 'cl)
> (require 'span)
> (require 'proof-syntax)
> - (require 'outline)
> - (defvar plastic-keymap nil))
> + (require 'outline))
> +(defvar plastic-keymap) ;FIXME: Not defined anywhere!
>
> (require 'plastic-syntax)
>
> diff --git a/pg-init.el b/pg-init.el
> index a6405361..3a2e5492 100644
> --- a/pg-init.el
> +++ b/pg-init.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
> @@ -42,25 +42,10 @@
> ;;; Code:
>
> ;;;###autoload
> -(eval-and-compile
> - (defvar pg-init--script-full-path
> - (or (and load-in-progress load-file-name)
> - (bound-and-true-p byte-compile-current-file)
> - (buffer-file-name)))
> - (defvar pg-init--pg-root
> - (file-name-directory pg-init--script-full-path)))
> -
> -;;;###autoload
> -(unless (bound-and-true-p byte-compile-current-file)
> - ;; This require breaks compilation, so it must only run when loading the
> package.
> - (require 'proof-site (expand-file-name "generic/proof-site"
> pg-init--pg-root)))
> -
> -(eval-when-compile
> - (let ((byte-compile-directories
> - '("generic" "lib"
> - "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox")))
> - (dolist (dir byte-compile-directories)
> - (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
> +(if t (require 'proof-site
> + (expand-file-name "generic/proof-site"
> + (file-name-directory
> + (or load-file-name buffer-file-name)))))
>
> (provide 'pg-init)
> ;;; pg-init.el ends here
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
