From a921439a4eb5b0d96182748e779c78e2f6a41a5f Mon Sep 17 00:00:00 2001
From: Stefan Monnier
Date: Tue, 11 Dec 2018 18:48:51 -0500
Subject: Cleanup patch; Moving defvar to toplevel

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.
---
 hol-light/hol-light.el | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'hol-light')

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)
-- 
cgit v1.2.3


From 632a3d7f9ded16faaf58e1c0769bcd4f7c8193e3 Mon Sep 17 00:00:00 2001
From: Stefan Monnier
Date: Wed, 12 Dec 2018 15:20:08 -0500
Subject: Use `cl-lib` instead of `cl` everywhere

Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.

* coq/coq-db.el: Use lexical-binding.

* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.

* coq/coq.el: Require `span` to silence some warnings.

* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.

* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.

* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.

* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!

* lib/holes.el: Use lexical-binding.
Remove redundant :group args.

* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.
---
 hol-light/hol-light-autotest.el | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'hol-light')

diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index d68b898f..dab2c4c4 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-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, 2012, 2014, 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
@@ -16,9 +16,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl))
-
 (require 'proof-site)
 (proof-ready-for-assistant 'hol-light)
 
-- 
cgit v1.2.3