NonGNU-devel ELPA: proof-general

-*- outline -*-  

This is a summary of main changes.  For details, please see
the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG

* Changes of Proof General 4.6 from Proof General 4.5

** Generic changes
*** Improve the omit-proofs feature to handle a number of cases where
    proofs must not be omitted.
*** Renew support for proof-tree visualization via the external command
    prooftree, see http://askra.de/software/prooftree and Section 7
    "Graphical Proof-Tree Visualization" in the Proof General manual.
    Proof-tree visualization is currently only supported for Coq. The
    prooftree support has been substantially rewritten, making use of
    the much better support since Coq version 8.11.
*** New command `proof-check-report' to generates the proof status
    of all opaque proofs. Currently only available for Coq, see Coq
    changes below for more details.
*** New command `proof-check-annotate' to annotate all failing proofs
    with FAIL comments.
*** Don't ask about killing the proof assistant when quitting Emacs and
    thereby the Proof General session.
*** Improve splash screen, add menu entry to permanently disable it
    (Proof-General -> Quick Options -> Display -> Disable Splash Screen),
    reduce splash screen time to make it less annoying
*** Goals windows tell when the goals continue out of view, with
    arrows in the fringe, see `proof-goals-indicators-enable'.
    Scrolling the goals stops at their end, see
    `proof-goals-scroll-margin'.
*** The double-hit terminator is available to every proof assistant:
    two quick hits process the script, see `proof-double-hit-enable'.
    It is an alternative to the unchanged electric terminator.

** Coq changes
*** Fewer files in coq/: the code of coq-diffs.el is in coq-goals.el,
    of coq-abbrev.el in coq.el, of coq-local-vars.el in coq-project.el.
    The old files remain as compatibility files, which will be removed:
    require the new ones instead.  `with-eval-after-load' of the old
    features still works.  The unused coq-autotest.el is removed.
*** Storing the goals or the response again (C-c C-a g, C-c C-a r)
    updates the window that displays *response-freeze*, instead of
    opening a new frame each time.
*** The Coq program, compiler and dependency analyzer given by file or
    directory variables (`coq-prog-name', `coq-compiler',
    `coq-dependency-analyzer') are no longer replaced by the detected
    ones when Coq starts.
*** The options `coq-use-makefile' and `coq-pre-v85', deprecated and
    unused, are removed: use `coq-pinned-version' instead of the
    latter.
*** Key bindings defined in `coq-mode-map' apply to all Coq backends,
    those in `proof-mode-map' only to Proof General: to keep your key
    bindings with another backend, define them in `coq-mode-map',
    preferably on commands common to all backends (see the manual).
    Those for the commands of `coq-all-buffers-commands' (queries,
    display, printing options) apply also in the goals and response
    buffers.  Each Coq interaction backend can add commands whose
    bindings in `coq-mode-map' apply also in the goals and response
    buffers that it manages.  The Proof General backend adds its
    all-buffer commands, processing and retracting the script, and
    highlighting a hypothesis.  C-c C-a C-r and C-c C-a C-g store the
    response and the goals in the goals buffer too, not only in the
    response buffer.
*** The toggle commands of the user options of Proof General
    (`proof-three-window-toggle', `proof-electric-terminator-toggle'…),
    of `coq-show-proof-stepwise' and of `coq-auto-adapt-printing-width'
    (new `coq-auto-adapt-printing-width-toggle'), and `coq-Compile', are
    defined without the proof shell, for all Coq backends.
*** The menus of the queries, of the printing options, of the
    abbreviations and of the project file are shared by all Coq
    backends: `coq-queries-menu-entries', `coq-other-queries-menu',
    `coq-options-menu', `coq-abbrevs-menu' and
...
...