diff options
81 files changed, 1814 insertions, 511 deletions
diff --git a/.travis.yml b/.travis.yml index 1f6c6833..6f70e507 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,5 @@ language: emacs-lisp -sudo: false +sudo: true env: - EMACS_TARGET=emacs-24.3 @@ -7,6 +7,7 @@ env: - EMACS_TARGET=emacs-24.5 - EMACS_TARGET=emacs-25.1 - EMACS_TARGET=emacs-25.2 + - EMACS_TARGET=emacs-25.3 before_install: - make -f Makefile.travis before_install @@ -1,22 +1,25 @@ Current Authors/Maintainers: - David Aspinall (all) - Pierre Courtieu (coq) - Erik Martin-Dorel (coq, website) - Clément Pit-Claudel (coq) - Christoph Raffalli (phox) - Makarius Wenzel (isar) + Pierre Courtieu (Coq, lib) + Erik Martin-Dorel (Coq, Web site) + Clément Pit-Claudel (Coq, packaging) + Henrik Tews (Proof Tree) Previous Authors: - Stefan Berghofer (isar) - Paul Callaghan (plastic,lego) - Healfdene Goguen (coq, generic, doc) - Thomas Kleymann (lego, doc, generic) - Patrick Loiseleur (coq) - David von Oheimb (x-symbol) - Dilip Sequeira (lego) - Graham Dutton (web support) + David Aspinall (all) + Christoph Raffalli (PhoX) + Makarius Wenzel (Isar, generic) + Stefan Berghofer (Isar) + Paul Callaghan (Plastic, Lego) + Healfdene Goguen (Coq, generic, doc) + Thomas Kleymann (Lego, doc, generic) + Patrick Loiseleur (Coq) + Stefan Monnier (Coq) + Yves Bertot (generic) + David von Oheimb (X-Symbol) + Dilip Sequeira (Lego, generic) + Graham Dutton (Web support) These are the main "official" authors of Proof General, but many more people have contributed, some very significantly. We're grateful to @@ -11,6 +11,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac *** bug fixes - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. + - cheat face (admit etc) now visible when locked. *** remove key-binding for proof-electric-terminator-toggle - The default key-binding for proof-electric-terminator-toggle @@ -18,6 +19,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac useful as we can expect users to configure electric-terminator once and for all. Hence the removal of this default key-binding. +*** add another (fallback) key-binding for proof-goto-point + - The default key-binding for proof-goto-point (C-c <C-return>) + was not available in TTYs. Now, this function can also be run + with "C-c RET", which happens to be automatically trigerred if + we type "C-c <C-return>" in a TTY. + ** Coq changes *** new menu Coq -> Auto Compilation for all background compilation options @@ -38,6 +45,55 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac compilation does not stop at the first error but rather continues as far as possible. +*** Limited extensibility for indentation + + Coq indentation mechanism is based on a fixed set of tokens and + precedence rules. Extensibility is now possible by adding new + syntax for a given token (no new token can be added). + + Typical example: if you define a infix operator xor you may + want to define it as a new syntax for token \/ in order to + have the indentation rules of or applied to xor. + + Use: + (setq coq-smie-user-tokens '(("xor" . "\\/"))) + + The set of tokens can be seen in variable smie-grammar. + +*** Clickable Hypothesis in goals buffer to copy/paste hyp names + + Clicking on a hyp name in goals buffer with button 2 copies its + name at current point position (which should be in the scripting + buffer). This eases the insertion of hypothesis names in scripts. + +*** Folding/unfolding hypothesis + + A cross "-" is displayed to the left of each hypothesis of the + goals buffer. Clicking ont it (button 1) hides/unhides the + hypothesis. You can also hit "f" while ont he hypothesis. "F" + unfolds all hypothesis. + + Hide/ unhide status remains when goal changes. + + +*** Highlighting of hypothesis + + You can highlight hypothesis in goals buffer on a per name + fashion. Hit "h" while on the hypothesis. "H" removes all + highlighting in the buffer. + + Highlighting status remains when goal changes. + + +**** Automtic highlighting with (search)About. + Hypothesis cited in the response buffer after C-c C-a C-a (i.e. + M-x coq-SearchAbout) will be highlighted automatically. Any other + hypothesis highlighted is unhighlighted. + + To disable this, do: + + (setq coq-highlight-hyps-cited-in-response nil) + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some @@ -57,7 +57,7 @@ Detailed installation Notes for Proof General Supported Emacs Versions. ------------------------- -Please see COMPATIBILTY. +Please see COMPATIBILITY. If you're not sure of your version of Emacs, inspect the variable `emacs-version' by doing: diff --git a/Makefile.travis b/Makefile.travis index 99c05dba..57efb391 100644 --- a/Makefile.travis +++ b/Makefile.travis @@ -1,4 +1,4 @@ -VERSIONS = 24.1 24.2 24.3 24.4 24.5 25.1 25.2 +VERSIONS = 24.1 24.2 24.3 24.4 24.5 25.1 25.2 25.3 STABLE_TARGETS = $(addprefix prepare-emacs-,$(VERSIONS)) .PHONY: prepare-emacs-24 prepare-emacs-git $(STABLE_TARGETS) \ @@ -15,6 +15,7 @@ prepare-emacs-git: cd /tmp/emacs && ./autogen.sh prepare-emacs: prepare-$(EMACS_TARGET) + echo 0 | sudo tee /proc/sys/kernel/randomize_va_space cd /tmp/emacs && ./configure --prefix="$(HOME)" --without-all --with-x-toolkit=no --without-x --with-xml2 && make -j2 install before_install: prepare-emacs @@ -2,12 +2,28 @@ [](https://travis-ci.org/ProofGeneral/PG) +## Overview + Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants. This is version 4.4.1~pre of Proof General. +## About Proof General branches + +Two editions of Proof General are currently available: + +* the (legacy) REPL-based, stable version of Proof General, + gathered in the + [master](https://github.com/ProofGeneral/PG/tree/master) branch, and + licensed under GPLv2; +* the (newest) Coq-specific, experimental version of Proof General, + supporting asynchronous proof processing, + gathered in the + [async](https://github.com/ProofGeneral/PG/tree/async) branch, and + licensed under GPLv3+. + ## Setup Remove old versions of Proof General, then download and install the new release from GitHub: @@ -57,3 +73,12 @@ Supported proof assistants: * Obsolete instances: Demoisa, Lambda-Clam, Plastic A few example proofs are included in each prover subdirectory. + +## Contributing + +Contributions to this repository are placed under the BSD-3 license. +As BSD-3 is compatible with both GPLv2 and GPLv3+, this means that +we can merge them in both `master` and `async` branches if need be, +using the same license as the rest of the codebase, while you keep +all the rights on your code. +For more info, see <https://opensource.org/licenses/BSD-3-Clause>. diff --git a/acl2/acl2.el b/acl2/acl2.el index 4f023217..cf9f521c 100644 --- a/acl2/acl2.el +++ b/acl2/acl2.el @@ -1,15 +1,25 @@ -;; acl2.el Basic Proof General instance for ACL2 -;; -;; Copyright (C) 2000 LFCS Edinburgh. +;;; acl2.el --- Basic Proof General instance for ACL2 + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> -;; -;; $Id$ + +;;; Commentary: ;; ;; Needs improvement! ;; ;; See the README file in this directory for information. +;;; Code: (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3a750472..5a555df5 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -1,10 +1,23 @@ ;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode -;; -;; Copyright (C) 1994-2009 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Healfdene Goguen, Pierre Courtieu +;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: ;; -;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + +;;; Code: (require 'proof) (require 'coq-syntax) diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index e3c4b978..9126c2ae 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -1,9 +1,20 @@ -;; coq-autotest.el: tests of Coq Proof General (in progress). +;;; coq-autotest.el --- tests of Coq Proof General (in progress). + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: ;; ;; You can run these by issuing "make test.coq" in PG home dir. ;; -;; $Id$ -;; + +;;; Code: (eval-when-compile (require 'cl)) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index f96b07da..c94cd8b7 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -1,17 +1,26 @@ -;; coq-compile-common.el --- common part of compilation feature -;; Copyright (C) 1994-2012 LFCS Edinburgh. +;;; coq-compile-common.el --- common part of compilation feature + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Hendrik Tews <hendrik@askra.de> -;; -;; $Id$ -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;;; Commentary: ;; ;; This file holds constants, options and some general functions for ;; the compilation feature. ;; +;;; Code: (require 'proof-shell) (require 'coq-system) diff --git a/coq/coq-db.el b/coq/coq-db.el index 0d9c0a6e..dccdca52 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -1,9 +1,18 @@ -;;; coq-db.el --- coq keywords database utility functions -;; +;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*- + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: Pierre Courtieu <courtieu@lri.fr> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; + ;;; Commentary: ;; ;; We store all information on keywords (tactics or command) in big @@ -284,19 +293,20 @@ See `coq-syntax-db' for DB structure." (defface coq-solve-tactics-face (proof-face-specs (:foreground "red") ; pour les fonds clairs - (:foreground "red") ; pour les fond foncés + (:foreground "red1") ; pour les fonds foncés ()) ; pour le noir et blanc "Face for names of closing tactics in proof scripts." :group 'proof-faces) -;;A new face for cheating tactics -;; FIXMe: the background color disappear when locked region overrides it. -;; this is hard to fix without re-colorizing afterward. +;;A face for cheating tactics +;; We use :box in addition to :background because box remains visible in +;; locked-region. :reverse-video is another solution. (defface coq-cheat-face - (proof-face-specs - (:background "red") ; pour les fonds clairs - (:background "red") ; pour les fond foncés - ()) ; pour le noir et blanc + '(;(((class color) (background light)) . (:inverse-video t :foreground "red" :background "black")) + ;(((class color) (background dark)) . (:inverse-video t :foreground "red1")) + (((class color) (background light)) . (:box (:line-width -1 :color "red" :style nil) :background "red")) + (((class color) (background dark)) . (:box (:line-width -1 :color "red1" :style nil) :background "red1")) + (t . ())) ; monocolor or greyscale: no highlight "Face for names of cheating tactics in proof scripts." :group 'proof-faces) @@ -306,7 +316,7 @@ See `coq-syntax-db' for DB structure." :group 'proof-faces) (defface coq-symbol-face - '((t :inherit default-face :bold coq-bold-unicode-binders)) + '((t :inherit font-lock-type-face :bold coq-bold-unicode-binders)) "Face for unicode binders, by default a bold version of `font-lock-type-face'." :group 'proof-faces) @@ -320,6 +330,28 @@ See `coq-syntax-db' for DB structure." "Face used for `ltac:', `constr:', and `uconstr:' headers." :group 'proof-faces) +;; This messes columns, can't figure out why putting this face makes the overlay +;; larger than a character +;; (defface coq-button-face +;; '((t :inherit custom-button :background "dark gray")) +;; "" +;; :group 'proof-faces) + +;; (defface coq-button-face-pressed +;; '((t :inherit custom-button-pressed :background "light gray")) +;; "" +;; :group 'proof-faces) + +(defface coq-button-face + '((t . (:background "light gray"))) + "" + :group 'proof-faces) + +(defface coq-button-face-pressed + '((t . (:background "dark gray"))) + "" + :group 'proof-faces) + (defconst coq-solve-tactics-face 'coq-solve-tactics-face "Expression that evaluates to a face. Required so that 'coq-solve-tactics-face is a proper facename") diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 878fb895..405cbb46 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -1,9 +1,17 @@ ;;; coq-indent.el --- indentation for Coq -;; -;; Copyright (C) 2004-2006 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Pierre Courtieu ;; Maintainer: Pierre Courtieu <courtieu@lri.fr> -;; + ;; Commentary: ;; ;; Indentation for Coq. @@ -104,13 +112,19 @@ detect if they start something or not." No context checking.") +;; Goal selector syntax +(defconst coq-goal-selector-regexp "[0-9]+\\s-*:\\s-*") + ;; We can detect precisely bullets (and curlies) by looking at there ;; prefix: the prefix should be a real "." then spaces then only ;; bullets and curlys and spaces). This is used when search backward. ;; This variable is the regexp of possible prefixes (defconst coq-bullet-prefix-regexp (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp "\\)" - "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)")) + "\\(?:\\.\\)\\(?:\\s-\\)" + "\\(?:\\s-\\|" + "\\(?:" coq-goal-selector-regexp "\\)?" + "{\\|}\\|-\\|+\\|\\*\\)*\\)")) ;; matches regular command end (. and ... followed by a space or buffer end) ;; ". " and "... " are command endings, ".. " is not, same as in @@ -152,7 +166,9 @@ There are 2 substrings: * number 2 is the left context matched that is not part of the bullet" ) (defconst coq-curlybracket-end-command - "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)" + (concat "\\(?:\\(?1:" + "\\(?:" coq-bullet-prefix-regexp"\\)?" + "{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)") "Matches ltac curlies when searching backward. Warning: False positive. There are 3 substrings (2 and 3 may be nil): @@ -165,7 +181,10 @@ This matches more than real ltac curlies. See only when searching backward).") (defconst coq-curlybracket-end-command-backward - (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)") + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)" + "\\(?:\\(?:\\(?1:" "\\(?:" coq-goal-selector-regexp "\\)?{\\)" + "\\(?3:[^|]\\)\\)" + "\\|\\(?1:}\\)\\)\\)") "Matches ltac curly brackets when searching backward. This should match EXACTLY script structuring curlies. No false @@ -357,8 +376,28 @@ Comments are ignored, of course." (start (coq-find-not-in-comment-backward "[^[:space:]]"))) ;; we must find a "." to be sure, because {O} {P} is allowed in definitions ;; with implicits --> this function is recursive - (if (looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p) - (looking-at "\\.\\|\\`")))) + (cond + ;; "{" can be prefixed by a goal selector (coq-8.8). + ;; TODO: looking-back is supposed to be slow. Find something else? + ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t)) + (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t)) + (and (looking-at "[0-9]+:\\s-*{") nil t)) + (goto-char (match-beginning 0)); swallow goal selector + (coq-empty-command-p)) + ;; other bulleting syntax + ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p)) + ;; vernacular controls Time, Fail, Redirect, Timeout + ((or (and (looking-at "e\\>") (looking-back "\\<Tim") (- (point) 3)) + (and (looking-at "l\\>") (looking-back "\\<Fai") (- (point) 3)) + (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+")) + (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*"))) + (goto-char (match-beginning 0)) + (coq-empty-command-p)) + ;; not a bullet, we found something else, it should be either a + ;; dot or the beginning of the file, otherwise we are in the + ;; middle of a command + (t (looking-at "\\.\\|\\`")) + ))) ; slight modification of proof-script-generic-parse-cmdend (one of the diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index 50a1f626..a097043a 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -1,14 +1,22 @@ ;;; coq-local-vars.el --- local variable list tools for coq -;; -;; Copyright (C) 2006-2008 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Pierre Courtieu ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; -;; $Id$ -;; + ;;; Commentary: ;; +;;; Code: + (require 'local-vars-list) ; in lib directory (eval-when-compile @@ -19,7 +27,6 @@ (defvar coq-load-path)) -;;; Code: (defconst coq-local-vars-doc nil "Documentation-only variable. diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 1580febd..17fe12d5 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -1,11 +1,19 @@ -;; coq-par-compile.el --- parallel compilation of required modules -;; Copyright (C) 1994-2012 LFCS Edinburgh. +;;; coq-par-compile.el --- parallel compilation of required modules + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Hendrik Tews <hendrik@askra.de> -;; -;; $Id$ -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;;; Commentary: ;; ;; This file implements compilation of required modules. The @@ -24,6 +32,8 @@ ;; changing compilers, all compilation jobs must be terminated. This is ;; consistent with the fact that the _CoqProject file is not reparsed. +;;; Code: + (eval-when-compile (require 'proof-compat)) diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index f60baacf..8e83d1d4 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -1,9 +1,19 @@ -;; coq-par-test.el --- tests for parallel compilation -;; Copyright (C) 2016 Hendrik Tews +;;; coq-par-test.el --- tests for parallel compilation + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Hendrik Tews <hendrik@askra.de> -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;;; Commentary: ;; ;; This file file contains tests for `coq-par-job-needs-compilation'. @@ -18,6 +28,7 @@ ;; ;; - integrate into PG build and test(?) system +;;; Code: (require 'coq-par-compile) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index bf492f82..90bd3c3d 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -1,11 +1,19 @@ -;; coq-seq-compile.el --- sequential compilation of required modules -;; Copyright (C) 1994-2012 LFCS Edinburgh. +;;; coq-seq-compile.el --- sequential compilation of required modules + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Hendrik Tews <hendrik@askra.de> -;; -;; $Id$ -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;;; Commentary: ;; ;; This file implements compilation of required modules. The @@ -14,6 +22,7 @@ ;; proof-action-list and compiles one module after the other. ;; +;;; Code: (eval-when-compile (require 'proof-compat)) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 33ef19d1..59d84e36 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -1,10 +1,18 @@ ;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq -;; Copyright (C) 2014 Free Software Foundation, Inc +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Authors: Pierre Courtieu ;; Stefan Monnier ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + ;; License: GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later) ;;; Commentary: @@ -42,6 +50,19 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) +(defcustom coq-smie-user-tokens nil + "Alist of (syntax . token) pairs to extend the coq smie parser. +These are user configurable additional syntax for smie tokens. It +allows to define alternative syntax for smie token. Typical +example: if you define a infix operator \"xor\" you may want to +define it as a new syntax for token \"or\" in order to have the +indentation rules of or applied to xor. Other exemple: if you +want to define a new notation \"ifb\" ... \"then\" \"else\" then +you need to declare \"ifb\" as a new syntax for \"if\" to make +indentation work well." + :type '(alist :key-type string :value-type string) + :group 'coq) + (defun coq-string-suffix-p (str1 str2 &optional ignore-case) "Return non-nil if STR1 is a prefix of STR2. @@ -375,6 +396,9 @@ The point should be at the beginning of the command name." (defun coq-smie-forward-token () (let ((tok (smie-default-forward-token))) (cond + ((assoc tok coq-smie-user-tokens) + (let ((res (assoc tok coq-smie-user-tokens))) + (cdr res))) ;; @ may be ahead of an id, it is part of the id. ((and (equal tok "@") (looking-at "[[:alpha:]_]")) (let ((newtok (coq-smie-forward-token))) ;; recursive call @@ -481,7 +505,7 @@ The point should be at the beginning of the command name." ":= with" (goto-char p) ":= module"))) - ((member corresp '("Inductive" "CoInductive")) ":= inductive") + ((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive") ((equal corresp "let") ":= let") ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind ((or (looking-back "{" nil)) ":= record") @@ -492,6 +516,9 @@ The point should be at the beginning of the command name." (defun coq-smie-backward-token () (let* ((tok (smie-default-backward-token))) (cond + ((assoc tok coq-smie-user-tokens) + (let ((res (assoc tok coq-smie-user-tokens))) + (cdr res))) ;; Distinguish between "," from quantification and other uses of ;; "," (tuples, tactic arguments) ((equal tok ",") @@ -567,12 +594,28 @@ The point should be at the beginning of the command name." (goto-char (1- (point))) "{|") ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) - (save-excursion - (forward-char -1) - (let ((nxttok (coq-smie-backward-token))) ;; recursive call - (coq-is-cmdend-token nxttok)))) + (save-excursion + (forward-char -1) + (if (and (looking-at "{") + (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (goto-char (match-beginning 0))) + (let ((nxttok (coq-smie-backward-token))) ;; recursive call + (coq-is-cmdend-token nxttok)))) (forward-char -1) - (if (looking-at "{") "{ subproof" "} subproof")) + (if (looking-at "}") "} subproof" + (if (and (looking-at "{") + (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (goto-char (match-beginning 0))) + "{ subproof" + )) + + ;; ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) + ;; (save-excursion + ;; (forward-char -1) + ;; (let ((nxttok (coq-smie-backward-token))) ;; recursive call + ;; (coq-is-cmdend-token nxttok)))) + ;; (forward-char -1) + ;; (if (looking-at "{") "{ subproof" "} subproof")) ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil)) ": ltacconstr") @@ -599,6 +642,9 @@ The point should be at the beginning of the command name." ((member tok '("*;" "-*;" "|-*;" "*|-*;")) ;; FIXME; can be "; ltac" too (forward-char (- (length tok) 1)) "; tactic") + ;; bullet detected, is it really a bullet? we have to traverse + ;; recursively any other bullet or "n:{" "}". this is the work of + ;; coq-empty-command-p ((and (string-match coq-bullet-regexp-nospace tok) (save-excursion (coq-empty-command-p))) (concat tok " bullet")) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 156d39e1..c55c93fc 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,10 +1,23 @@ -;; coq-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007, 2009 LFCS Edinburgh. +;;; coq-syntax.el --- Font lock expressions for Coq + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; coq-syntax.el,v 11.13 2013/07/10 14:59:08 pier Exp +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; + +;;; Code: (require 'proof-syntax) (require 'proof-utils) ; proof-locate-executable @@ -490,6 +503,7 @@ so for the following reasons: ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") + ("Variant" "varv" "Variant # : # := # : #." t "Variant") ) "Coq definition keywords information list. See `coq-syntax-db' for syntax. " ) @@ -516,7 +530,7 @@ so for the following reasons: ("Instance goal" "instg" "Instance #:#.\n#\nDefined." t);; careful ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Proposition" "l" "Proposition # : #.\nProof.\n#\nQed." t "Proposition") + ("Proposition" "pr" "Proposition # : #.\nProof.\n#\nQed." t "Proposition") ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful @@ -1341,12 +1355,72 @@ It is used: (proof-zap-commas)))) -;; ", " is for multiple hypothesis displayed in v8.5. If more than -;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) -;; "^ " is for goals in debug mode. +;; ", " is for multiple hypothesis displayed in v8.5. +;; exactly no space after start of line = hyps names in +;; Search results (and when we get a more compact display of hyps) +;; exactly 2 spaces at start of line = is for normal goal display at +;; start of line +;; exactly 3 spaces at start of line = hyps on the same line (Set +;; Printing Compact Goals". +;; If more than 3 spaces: not a hyp. +;; we used to have: "^ " for goals in debug mode but it does not seem +;; necessary anymore. (defvar coq-hyp-name-in-goal-or-response-regexp - "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(\\(?:[^\n :(),=]\\|, \\)+ *\\(?::[ \n]\\|,$\\)\\)" - "regexp matching hypothesis names in goal or response buffer") + "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ] \\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\)\\(?: *:=?[ \n]\\|,$\\)" + "regexp matching hypothesis names in goal or response buffer. +Subexpr 2 contains the real name of the function. +Subexpr 1 contains the prefix context (spaces mainly) that is not +part of another hypothesis.") + +; Matches the end of the last hyp, before the ======... separator. +(defvar coq-hyp-name-or-goalsep-in-goal-or-response-regexp + (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)")) + +(defun coq-find-first-hyp () + (with-current-buffer proof-goals-buffer + (save-excursion + (goto-char (point-min)) + (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (match-beginning 2)))) + +(defun coq-detect-hyps-positions (buf &optional limit) + "Detect all hypothesis displayed in buffer BUF and returns positions. +5 positions are created for each hyp: (begcross beghypname +endhypname beg end)." + (with-current-buffer buf + (save-excursion + (goto-char (point-min)) + (let ((res '())) + (goto-char (point-min)) + (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp limit t) + (let* ((str (replace-regexp-in-string "\\`[ \r\n\t]+\\|[ \r\n\t]+\\'" "" (match-string 2) t t)) + (beghypname (match-beginning 2)) + (beg (match-end 0)) + (begcross (match-beginning 1)) + (endhypname (match-end 2)) + (splitstr (split-string str ",\\|,$\\|:" t)) ; 4th arg of split-string errors in emacs24 + (end (save-excursion ; looking for next hyp and return its leftest part + (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) + (goto-char (match-beginning 1)) + ;; if previous is a newline, don't include it i the overklay + (when (looking-back "\\s-") (goto-char (- (point) 1))) + (point)))) + ; if several hyp names, we name the overlays with the first hyp name + (setq res + (cons + (cons (mapcar (lambda (s) (substring-no-properties s)) splitstr) + (list begcross beghypname endhypname beg end)) + res)))) + res)))) + +;; Don't look at the conclusion of the goal +(defun coq-detect-hyps-positions-in-goals () + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (coq-detect-hyps-positions + proof-goals-buffer + (if (search-forward-regexp "==========" nil t) (point) nil)))) + ;; We define a slightly different set of keywords for response buffer. diff --git a/coq/coq-system.el b/coq/coq-system.el index 8da4ea23..93c9dd7e 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -1,9 +1,18 @@ -;; coq-system.el --- common part of compilation feature -;; Copyright (C) 2015 LFCS Edinburgh. +;;; coq-system.el --- common part of compilation feature + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre.Courtieu<Pierre.Courtieu@cnam.fr> -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; @@ -12,6 +21,8 @@ ;; support for older versions of coq. ;; +;;; Code: + (require 'proof) (eval-when-compile @@ -22,8 +33,17 @@ (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 +;; (defpgcustom prog-args) declaration. +(defun coq--string-list-p (obj) + "Determine if OBJ is a list of strings." + (or (null obj) (and (consp obj) (stringp (car obj)) (coq--string-list-p (cdr obj))))) + +(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p) + (defcustom coq-prog-env nil - "List of environment settings d to pass to Coq process. + "List of environment settings to pass to Coq process. On Windows you might need something like: (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))" :group 'coq) @@ -322,9 +342,9 @@ request compatibility handling of flags." ((or `(rec ,dir ,alias) `(,dir ,alias)) (list "-R" (expand-file-name dir) alias))))) -(defun coq-include-options (load-path &optional current-directory pre-v85) +(defun coq-include-options (loadpath &optional current-directory pre-v85) "Build the base list of include options for coqc, coqdep and coqtop. -The options list includes all entries from argument LOAD-PATH +The options list includes all entries from argument LOADPATH \(which should be `coq-load-path' of the buffer that invoked the compilation) prefixed with suitable options and (for coq<8.5), if `coq-load-path-include-current' is enabled, the directory base of @@ -335,12 +355,12 @@ CURRENT-DIRECTORY should be an absolute directory name. It can be nil if `coq-load-path-include-current' is nil. A non-nil PRE-V85 flag requests compatibility handling of flags." - (unless (coq-load-path-safep load-path) + (unless (coq-load-path-safep loadpath) (error "Invalid value in coq-load-path")) (when (and pre-v85 coq-load-path-include-current) (cl-assert current-directory) - (push current-directory load-path)) - (cl-loop for entry in load-path + (push current-directory loadpath)) + (cl-loop for entry in loadpath append (coq-option-of-load-path-entry entry pre-v85))) (defun coq--options-test-roundtrip-1 (coq-project parsed pre-v85) @@ -374,31 +394,31 @@ options of a few coq-project files does the right thing." (coq--options-test-roundtrip "-R /test Test") (coq--options-test-roundtrip "-I /test"))) -(defun coq-coqdep-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85) "Build a list of options for coqdep. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." - (coq-include-options load-path current-directory pre-v85)) +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." + (coq-include-options loadpath current-directory pre-v85)) -(defun coq-coqc-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqc-prog-args (loadpath &optional current-directory pre-v85) "Build a list of options for coqc. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." ;; coqtop always adds the current directory to the LoadPath, so don't ;; include it in the -Q options. (append (remove "-emacs" coq-prog-args) (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3 - (coq-coqdep-prog-args coq-load-path current-directory pre-v85)))) + (coq-coqdep-prog-args loadpath current-directory pre-v85)))) ;;XXXXXXXXXXXXXX ;; coq-coqtop-prog-args is the user-set list of arguments to pass to ;; Coq process, see 'defpacustom prog-args' in pg-custom.el for ;; documentation. -(defun coq-coqtop-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqtop-prog-args (loadpath &optional current-directory pre-v85) ;; coqtop always adds the current directory to the LoadPath, so don't ;; include it in the -Q options. This is not true for coqdep. "Build a list of options for coqc. LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." - (cons "-emacs" (coq-coqc-prog-args load-path current-directory pre-v85))) + (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85))) (defun coq-prog-args () "Recompute `coq-load-path' before calling `coq-coqtop-prog-args'." @@ -407,8 +427,8 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." (coq-coqtop-prog-args coq-load-path)) (defcustom coq-use-project-file t - "If t, when opening a coq file read the dominating _CoqProject. -If t, when a coq file is opened, Proof General will look for a + "If t, when opening a Coq file read the dominating _CoqProject. +If t, when a Coq file is opened, Proof General will look for a project file (see `coq-project-filename') somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that @@ -480,7 +500,7 @@ Returns a mixed list of option-value pairs and strings." (arity (cdr (assoc switch coq--makefile-switch-arities)))) (push (coq--read-one-option-from-project-file switch arity raw-args) options) (setq raw-args (nthcdr (or arity 0) raw-args)))) - options)) + (nreverse options))) ; Order of options is important sometimes (Cf. #7980) (defun coq--extract-prog-args (options) "Extract coqtop arguments from _CoqProject options OPTIONS. diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index faa02458..5f2cd0c6 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -1,8 +1,17 @@ -;;; -*- coding: utf-8; -*- -;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -;; -;; Copyright(C) 2008, 2009 David Aspinall / LFCS Edinburgh +;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*- + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + +;;; Commentary: ;; ;; This file is loaded by `proof-unicode-tokens.el'. ;; @@ -1,12 +1,23 @@ -;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*- -;; Copyright (C) 1994-2009 LFCS Edinburgh. +;;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*- + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; -;; $Id$ +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;;; Commentary: +;; + +;;; Code: (eval-when-compile (require 'cl) @@ -42,7 +53,6 @@ (require 'coq-seq-compile) ; sequential compilation of Requires (require 'coq-par-compile) ; parallel compilation of Requires - ;; for compilation in Emacs < 23.3 (NB: declare function only works at top level) (declare-function smie-bnf->prec2 "smie") (declare-function smie-rule-parent-p "smie") @@ -78,7 +88,7 @@ ;; :group 'coq) (defcustom coq-user-init-cmd nil - "user defined init commands for Coq. + "User defined init commands for Coq. These are appended at the end of `coq-shell-init-cmd'." :type '(repeat (cons (string :tag "command"))) :group 'coq) @@ -91,12 +101,12 @@ These are appended at the end of `coq-shell-init-cmd'." ;; Default coq is only Private_ and _subproof (defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" - "String for blacklisting strings from requests to coq environment." + "String for blacklisting strings from requests to Coq environment." :type 'string :group 'coq) (defcustom coq-prefer-top-of-conclusion nil - "prefer start of the conclusion over its end when displaying goals + "Prefer start of the conclusion over its end when displaying goals that do not fit in the goals window." :type 'boolean :group 'coq) @@ -432,7 +442,8 @@ This is a subroutine of `proof-shell-filter'." (set-marker proof-shell-urgent-message-scanner (if end ;; couldn't find message start; move forward to avoid rescanning - (max initstart + (max (or lastend 1) ;; goto after last end urgent msg + ;; or near the end of current output if that jumps farther. (- (point) (1+ proof-shell-eager-annotation-start-length))) ;; incomplete message; leave marker at start of message @@ -884,7 +895,7 @@ Support dot.notation.of.modules." (if notation (concat "\"" notation "\"") "")))) (defcustom coq-remap-mouse-1 nil - "Wether coq mode should remap mouse button 1 to coq queries. + "Whether Coq mode should remap mouse button 1 to Coq queries. This overrides the default global binding of (control mouse-1) and (shift mouse-1) (buffers and faces menus). Hence it is nil by @@ -935,13 +946,14 @@ Otherwise propose identifier at point if any." nil 'proof-minibuffer-history guess))) -(defun coq-ask-do (ask do &optional dontguess postformatcmd) +(defun coq-ask-do (ask do &optional dontguess postformatcmd wait) "Ask for an ident and print the corresponding term." (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd))) (proof-shell-ready-prover) (setq cmd (coq-guess-or-ask-for-string ask dontguess)) (proof-shell-invisible-command - (format (concat do " %s . ") (funcall postform cmd))))) + (format (concat do " %s . ") (funcall postform cmd)) + wait))) (defun coq-flag-is-on-p (testcmd) @@ -1043,15 +1055,6 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "SearchRewrite" "SearchRewrite" nil)) -;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. -(defun coq-SearchAbout () - (interactive) - (coq-ask-do - ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: - ;; "_ind" "_rec" "R_" "_equation" - "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout") - (message "use [Coq/Settings/Search Blacklist] to change blacklisting.")) @@ -1063,6 +1066,11 @@ With flag Printing All if some prefix arg is given (C-u)." (coq-ask-do-show-all "Print" "Print") (coq-ask-do "Print" "Print"))) +(defun coq-Print-Ltac () + "Ask for an ident and print the corresponding Ltac term." + (interactive) + (coq-ask-do "Print Ltac" "Print Ltac")) + (defun coq-Print-with-implicits () "Ask for an ident and print the corresponding term." (interactive) @@ -1359,26 +1367,411 @@ goal is redisplayed." (rd (read-number (format "Width (%S): " deflt) deflt))) (coq-adapt-printing-width t rd))) +;;;;; utils fo overlays +(defun coq-overlays-at (pt prop) + (let ((overlays (overlays-at pt)) + found) + (while overlays + (let ((overlay (car overlays))) + (if (overlay-get overlay prop) + (setq found (cons overlay found)))) + (setq overlays (cdr overlays))) + found)) + +;;;;;;;;;; Hypothesis tracking ;;;;;;;;;; +;;; Facilities to build overlays for hyp names and hyp+type + hypcross +;;; ((un)folding buttons). +(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis") +(defvar coq-hypcross-map (make-sparse-keymap) "Keymap for visible hypothesis") + +(defvar coq-hypcross-hovering-help t + "Whether hyps fold cross pops up a help when hovered.") + +(defvar coq-hyps-positions nil + "The list of positions of hypothesis in the goals buffer. +Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") + +;; Hyps name are clickable and have a special keymap. +(defun coq-make-hypname-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypname t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypname-map)) + ov)) + +;; Hyps types are clickable only when folded +(defun coq-make-hyp-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hyp t) + (overlay-put ov 'hyp-name h)) + ov)) + +(defun coq-hypcross-unfolded-string() + (propertize + "-" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +(defun coq-hypcross-folded-string() + (propertize + "+" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +;; hypcross is displayerd with a "-" when unfolded and a "+" when unfolded. +;; It is highlighted when hovered, is clickable and have a special +;; keymap (f toggles folding, h toggles highlighting...). +;; PC: using button faces of make-button makes the button larger than a +;; characters, which messes columns. So we use simple background colors in +;; coq-hyp...faces +(defun coq-make-hypcross-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypcross t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypcross-map) + (overlay-put ov 'display (coq-hypcross-unfolded-string)) + ;(overlay-put ov 'face 'coq-button-face) + ;(overlay-put ov 'mouse-face 'coq-button-face-pressed) + ;(overlay-put ov 'width .6) + ;(overlay-put ov 'height -1) + (when (eq coq-hypcross-hovering-help t) + (overlay-put ov 'help-echo "mouse-3: unfold; mouse-2 copy name"))) + ov)) + +;; Once we have created the 3 overlays, each recieves a reference to the 2 +;; others. +(defun coq-hyp-overlay-build-cross-refs (hypnameov hypov crosshypov) + (overlay-put hypnameov 'hypcross-ov crosshypov) + (overlay-put hypov 'hypcross-ov crosshypov) + (overlay-put hypnameov 'hyp-ov hypov) + (overlay-put crosshypov 'hyp-ov hypov) + (overlay-put hypov 'hypname-ov hypnameov) + (overlay-put crosshypov 'hypname-ov hypnameov)) + +(defun coq-build-hyp-overlay (hyp-positions buf) + (let* ((names (car hyp-positions)) + (fstname (car names)) + (positions (cdr hyp-positions)) + (begcross (car positions)) + (beghypname (cadr positions)) + (endhypname (caddr positions)) + (beg (cadddr positions)) + (end (cadddr (cdr positions)))) + (let ((hypnameov (coq-make-hypname-overlay beghypname endhypname fstname buf)) + (hypov (coq-make-hyp-overlay beg end fstname buf)) + (crosshypov (coq-make-hypcross-overlay begcross (+ 1 begcross) fstname buf)) + res) + (coq-hyp-overlay-build-cross-refs hypnameov hypov crosshypov) + (mapc + (lambda (s) + (setq res + (cons + (cons (substring-no-properties s) + (cons hypov (cons hypnameov (cons crosshypov nil)) )) + res))) + names) + res))) + +(defun coq-build-hyps-overlays (hyp-positions buf) + (let ((res)) + (mapc (lambda (x) (let ((lassoc (coq-build-hyp-overlay x buf))) + (setq res (append lassoc res)))) + hyp-positions) + res)) + +; builds the list of names from one hyp position (which may contained several +; hyp names) +(defun coq-build-hyp-name (hyp-positions) + (let* ((names (car hyp-positions)) + res) + (mapc (lambda (s) (setq res (cons (substring-no-properties s) res))) names) + res)) + +;; Build the list of hyps names +(defun coq-build-hyps-names (hyp-positions) + (let ((res)) + (mapc (lambda (x) (let ((lassoc (coq-build-hyp-name x))) + (setq res (append lassoc res)))) + hyp-positions) + res)) + + +(defun coq-detect-hyps-in-goals () + "Detect all hypothesis displayed in goals buffer and create overlays. +Three overlays are created for each hyp: (hypov hypnameov hypcrossov), respectively +for the whole hyp, only its name and the overlay for fold/unfold cross. +Returnns the list of mappings hypname -> overlays. +" + (let* + ((fsthyp-pos (coq-find-first-hyp)) + (fsthyp-ov (when fsthyp-pos (with-current-buffer proof-goals-buffer + (overlays-at fsthyp-pos)))) + ; is there at least one hyp overlay there? + (fsthyp-hypov (when fsthyp-ov + (cl-some (lambda(x) (overlay-get x 'hyp-name)) + fsthyp-ov)))) + (if fsthyp-hypov coq-hyps-positions ;overlays are already there + (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) proof-goals-buffer)))) + +(defun coq-find-hyp-overlay (h) + (cadr (assoc h coq-hyps-positions))) + +;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;; +;; Feature: highlighting of hyptohesis that remains when the cript is played +;; (and goals buffer is updated). + +;; On by default. This only works with the SearchAbout function for now. +(defvar coq-highlight-hyps-cited-in-response t + "If non-nil, try to highlight in goals buffers hyps cited in response.") + +;; We maintain a list of hypothesis names that must be highlighted at each +;; regeneration of goals buffer. +(defvar coq-highlighted-hyps nil + "List of hypothesis names that must be highlighted. +These are rehighlighted at each regeneration of goals buffer +using a hook in `proof-shell-handle-delayed-output-hook'.") + +(defun coq-highlight-hyp-aux (h) + "Auxiliary function, use `coq-highlight-hyp' for sticky highlighting. +Unless you want the highlighting to disappear after the goals +buffer is updated." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay + (overlay-put hyp-overlay 'face '(:background "lavender"))))) + +(defun coq-unhighlight-hyp-aux (h) + "Auxiliary function, use `coq-unhighlight-hyp' for sticky highlighting. +Unless you want the highlighting to disappear after the goals +buffer is updated." + (let* ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay + (overlay-put hyp-overlay 'face nil)))) + +(defun coq-highlight-hyp (h) + "Highlight hypothesis named H (sticky). +use `coq-unhighlight-hyp' to unhilight." + (unless (member h coq-highlighted-hyps) + (setq coq-highlighted-hyps (cons h coq-highlighted-hyps))) + (coq-highlight-hyp-aux h)) + +(defun coq-unhighlight-hyp (h) + "Unhighlight hypothesis named H." + (when (member h coq-highlighted-hyps) + (setq coq-highlighted-hyps (delete h coq-highlighted-hyps)) + (coq-unhighlight-hyp-aux h))) + +(defun coq-highlight-hyps (lh) + (mapc 'coq-highlight-hyp lh)) + +(defun coq-unhighlight-hyps (lh) + (mapc 'coq-unhighlight-hyp-aux lh)) + +(defun coq-highlight-selected-hyps () + "Highlight all hyps stored in `coq-highlighted-hyps'. +This used in hook to rehilight hypothesis after goals buffer is +updated." + (interactive) + (coq-highlight-hyps coq-highlighted-hyps)) + +(defun coq-unhighlight-selected-hyps () + "Unhighlight all hyps stored in `coq-highlighted-hyps'. +This used before updating `coq-highlighted-hyps' with a new set +of hypothesis to highlight." + (interactive) + (coq-unhighlight-hyps coq-highlighted-hyps) + (setq coq-highlighted-hyps nil)) + +(defun coq-get-hyps-cited-in-response () + "Returns locations of hyps in goals buffer that are cited in response buffer. +See `coq-highlight-hyps-cited-in-response' and `SearchAbout'." + (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer)) + (hyps-cited (coq-build-hyps-names hyps-cited-pos))) + (remove-if-not + (lambda (e) + (cl-some;seq-find + (lambda (f) + (string-equal (car e) f)) + hyps-cited)) + coq-hyps-positions))) + +(defun coq-highlight-hyps-cited-in-response () + "Highlight hypothesis cited in response buffer. +Highlight always takes place in goals buffer." + (let ((inters (coq-get-hyps-cited-in-response))) + (coq-unhighlight-selected-hyps) + (setq coq-highlighted-hyps (mapcar 'car inters)) + (coq-highlight-selected-hyps))) + +(defun coq-toggle-highlight-hyp (h) + "Toggle the highlighting status of hypothesis H. +See `coq-highlight-hyp'." + (interactive "sHypothesis name to highlight:") + (if (member h coq-highlighted-hyps) + (coq-unhighlight-hyp h) + (coq-highlight-hyp h))) + +(defun coq-toggle-highlight-hyp-at (pt) + "Toggle hiding the hypothesis at point." + (interactive) + (let* ((ov + (or (car (coq-overlays-at pt 'hyp-name)) + ;; we may be between hypname and hyp, so skip backward to + ;; something meaningful + (save-excursion + (goto-char pt) + (search-backward-regexp "[^ :=]\\|\n") + (car (coq-overlays-at (point) 'hyp-name))))) + (hypname (and ov + (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-highlighted-hyps) + (coq-unhighlight-hyp hypname) + (coq-highlight-hyp hypname))))) + +(defun coq-toggle-highlight-hyp-at-point () + (interactive) + (coq-toggle-highlight-hyp-at (point))) + -(defvar coq-highlight-id-last-regexp nil) +(defun coq-insert-at-point-hyp-at-mouse (event) + (interactive "e") + (let ((hyp-name (save-excursion + (with-current-buffer proof-goals-buffer + (save-excursion + (overlay-get (car (overlays-at (posn-point (event-start event)))) + 'hyp-name)))))) + (insert hyp-name))) + +;;;;;;;;;;; Hiding Hypothesis ;;;;;;;;;;; +(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis") -(defun coq-highlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (highlight-regexp re 'lazy-highlight))) +(defvar coq-hidden-hyps nil + "List of hypothesis that should be hidden in goals buffer. +These are re-hidden at each regeneration of goals buffer +using a hook in `proof-shell-handle-delayed-output-hook'.") -(defun coq-unhighlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (unhighlight-regexp re))) -(defun coq-highlight-id-at-pt-in-goals () +(defun coq-toggle-fold-hyp-at (pt) + "Toggle hiding the hypothesis at point." (interactive) - (let* ((id (coq-id-or-notation-at-point)) - (re (regexp-quote (or id "")))) - (when coq-highlight-id-last-regexp - (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp)) - (coq-highlight-id-in-goals re) - (setq coq-highlight-id-last-regexp re))) + (let* ((ov (car (coq-overlays-at pt 'hyp-name))) + (hypname (and ov (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-hidden-hyps) + (coq-unfold-hyp hypname) + (coq-fold-hyp hypname))))) + +(defun coq-toggle-fold-hyp-at-point () + (interactive) + (coq-toggle-fold-hyp-at (point))) +(defun coq-toggle-fold-hyp-at-mouse (event) + "Toggle hiding the hypothesis at mouse click. +Used on hyptohesis overlays in goals buffer mainly." + (interactive "e") + (save-excursion + (with-current-buffer proof-goals-buffer + (save-excursion (coq-toggle-fold-hyp-at (posn-point (event-start event))))))) + +(defun coq-configure-hyp-overlay-hidden (hyp-overlay h) + (when hyp-overlay + (let* ((lgthhyp (- (overlay-end hyp-overlay) (overlay-start hyp-overlay))) + (prefx (make-string (min 8 lgthhyp) ?.)) + (hypcross-ov (overlay-get hyp-overlay 'hypcross-ov))) + (overlay-put + hyp-overlay 'display + prefx ;(propertize prefx 'keymap coq-hidden-hyp-map) + ) + (overlay-put hyp-overlay 'evaporate t) + (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face) + (overlay-put hyp-overlay 'help-echo "mouse-3: unfold; mouse-2 copy name") + (overlay-put hyp-overlay 'hyp-name h) + (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map) + (overlay-put hypcross-ov 'display (coq-hypcross-folded-string))))) + +(defun coq-configure-hyp-overlay-visible (hyp-overlay h) + (when hyp-overlay + (overlay-put hyp-overlay 'display nil) + (overlay-put hyp-overlay 'evaporate t) + (overlay-put hyp-overlay 'mouse-face nil) + (overlay-put hyp-overlay 'help-echo nil) + (overlay-put hyp-overlay 'keymap nil) + (overlay-put (overlay-get hyp-overlay 'hypcross-ov) 'display (coq-hypcross-unfolded-string)))) + +(defun coq-fold-hyp-aux (h) + "Fold hypothesis H's type from the context temporarily. +Displays \".......\" instead. This function relies on variable +coq-hyps-positions. The hiding is cancelled as soon as the goals +buffer is changed, consider using `coq-fold-hyp' if you want the +hiding to be maintain when scripting/undoing." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay (coq-configure-hyp-overlay-hidden hyp-overlay h)))) + +(defun coq-fold-hyp (h) + "Fold hypothesis H's type from the context durably. +(displays \".......\" instead). This function relies on variable +coq-hyps-positions. The hiding maintained as the goals buffer is +changed, thanks to a hook on +`proof-shell-handle-delayed-output-hook', consider using +`coq-fold-hyp' if you want the hiding to be maintain when +scripting/undoing." + (interactive) + (unless (member h coq-hidden-hyps) + (setq coq-hidden-hyps (cons h coq-hidden-hyps)) + (coq-fold-hyp-aux h))) + +(defun coq-unfold-hyp-aux (h) +"Unfold hypothesis H temporarily. +See `coq-fold-hyp-aux'." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (coq-configure-hyp-overlay-visible hyp-overlay h))) + +(defun coq-unfold-hyp (h) +"Unfold hypothesis H durably. +See `coq-fold-hyp'." + (interactive) + (when (member h coq-hidden-hyps) + (setq coq-hidden-hyps (delete h coq-hidden-hyps)) + (coq-unfold-hyp-aux h))) + +(defun coq-unfold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-unfold-hyp-aux'." + (mapc 'coq-unfold-hyp-aux lh)) + +(defun coq-fold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-fold-hyp-aux'." + (mapc 'coq-fold-hyp-aux lh)) + +(defun coq-fold-hyps () + "Fold the type of hypothesis in LH durably. +See `coq-fold-hyp'." + (interactive) + (coq-fold-hyp-list coq-hidden-hyps)) + + +(defun coq-unfold-hyps () + "Unfold the type of hypothesis in LH durably. +See `coq-unfold-hyp'." + (interactive) + (coq-unfold-hyp-list coq-hidden-hyps) + (setq coq-hidden-hyps nil)) + +(defun coq-toggle-fold-hyp (h) + "Toggle the hiding status of hypothesis H (asked interactively). +See `coq-fold-hyp'." + (interactive "sHypothesis to fold: ") + (if (member h coq-hidden-hyps) + (coq-unfold-hyp h) + (coq-fold-hyp h))) +;;;;;;; (proof-definvisible coq-PrintHint "Print Hint. ") @@ -1840,7 +2233,7 @@ Near here means PT is either inside or just aside of a comment." (defpacustom search-blacklist coq-search-blacklist-string - "Strings to blacklist in requests to coq environment." + "Strings to blacklist in requests to Coq environment." :type 'string :get 'coq-get-search-blacklist :setting coq-set-search-blacklist) @@ -2394,6 +2787,21 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (proof-shell-invisible-command q)))) +;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. +(defun coq-SearchAbout () + (interactive) + (coq-ask-do + ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: + ;; "_ind" "_rec" "R_" "_equation" + "SearchAbout (ex: \"eq_\" eq -bool)" + "SearchAbout" + nil nil t) + (when coq-highlight-hyps-cited-in-response + (coq-highlight-hyps-cited-in-response) + (message "M-x coq-unhighlight-selected-hyps to remove highlighting, [Coq/Settings/Search Blacklist] to change blacklisting.")) + (unless coq-highlight-hyps-cited-in-response + (message "[Coq/Settings/Search Blacklist] to change blacklisting."))) + ;; Insertion commands (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) @@ -2443,6 +2851,11 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-ask-adapt-printing-width-and-show) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation) +;; specific to goals buffer: (un)foldinng and (un)highlighting shortcuts +(define-key coq-goals-mode-map [?f] 'coq-toggle-fold-hyp-at-point) +(define-key coq-goals-mode-map [?F] 'coq-unfold-hyps) +(define-key coq-goals-mode-map [?h] 'coq-toggle-highlight-hyp-at-point) +(define-key coq-goals-mode-map [?H] 'coq-unhighlight-selected-hyps) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -2481,6 +2894,27 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key proof-goals-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) (define-key proof-goals-mode-map [(control shift mouse-1)] '(lambda () (interactive)))) + + +;; Default binding on hypothesis names: clicking on the name of an hyp with +;; button 3 folds it. Click on it with button 2 copies the names at current +;; point. +(when coq-hypname-map + (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) + +;; Default binding: clicking on the cross to folds/unfold hyp. +;; Click on it with button 2 copies the names at current point. +(when coq-hypname-map + (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point) + (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) +;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with +;; button 2 it copies hyp name at current point. +(when coq-hidden-hyp-map + (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) + ;;;;;;;;;;;;;;;;;;;;;;;; ;; error handling ;;;;;;;;;;;;;;;;;;;;;;;; @@ -2626,7 +3060,7 @@ number of hypothesis displayed, without hiding the goal" (with-selected-window goal-win ;; find snd goal or buffer end, if not found this goes to the ;; end of buffer - (search-forward-regexp "subgoal 2\\|\\'") + (search-forward-regexp "subgoal 2\\|\\*\\*\\* Unfocused goals:\\|\\'") (beginning-of-line) ;; find something backward else than a space: bottom of concl (ignore-errors (search-backward-regexp "\\S-")) @@ -2683,6 +3117,14 @@ number of hypothesis displayed, without hiding the goal" proof-shell-last-output) (proof-clean-buffer proof-goals-buffer)))) +(add-hook 'proof-shell-handle-delayed-output-hook + (lambda () + (setq coq-hyps-positions (coq-detect-hyps-in-goals)) + (coq-highlight-selected-hyps) + (coq-fold-hyps) + )) + + (defun is-not-split-vertic (selected-window) (<= (- (frame-height) (window-height)) 2)) diff --git a/coq/coqtags b/coq/coqtags index 50d4a2f5..6a6e5a64 100755 --- a/coq/coqtags +++ b/coq/coqtags @@ -59,10 +59,10 @@ while(<>) elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) { adddecs($stmt,$1); } - elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record))\s+([\w\']+))/) + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record)|(Variant))\s+([\w\']+))/) { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; - if($2 eq "Inductive" || $2 eq "CoInductive"){ + if($2 eq "Inductive" || $2 eq "CoInductive" || $2 eq "Variant"){ add_constructors($stmt); } elsif($2 eq "Record"){ diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index 1d074d8d..614b56e2 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.el @@ -1,13 +1,24 @@ -;; doc/docstring-magic.el -- hack for using texi-docstring-magic. -;; -;; Copyright (C) 1998 LFCS Edinburgh. +;;; doc/docstring-magic.el --- hack for using texi-docstring-magic. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> + +;;; Commentary: ;; ;; Ensure that non-compiled versions of everything are loaded. ;; -;; $Id$ -;; + +;;; Code: + (setq load-path (append '("../generic/") load-path)) (load "proof-site.el") diff --git a/etc/emacsbugs/visiblity-attempt.el b/etc/emacsbugs/visiblity-attempt.el index ad88799c..b6486116 100644 --- a/etc/emacsbugs/visiblity-attempt.el +++ b/etc/emacsbugs/visiblity-attempt.el @@ -1,6 +1,21 @@ -;;; -;;; === Test area for invisibility === -;;; +;;; visiblity-attempt.el --- Test area for invisibility + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: +;; +;; Test area for invisibility +;; + +;;; Code: + (defvar vis nil) (overlay-put (make-overlay 18 22) 'invisible 'smaller) diff --git a/etc/lego/lego-site.el b/etc/lego/lego-site.el index 55098331..1a31f354 100644 --- a/etc/lego/lego-site.el +++ b/etc/lego/lego-site.el @@ -1,8 +1,22 @@ -;;; lego-site.el Site-specific Emacs support for LEGO -;;; Copyright (C) 1998 LFCS Edinburgh +;;; lego-site.el --- Site-specific Emacs support for LEGO + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;;; Author: Thomas Kleymann <T.Kleymann@ed.ac.uk> ;;; Maintainer: lego@dcs.ed.ac.uk +;;; Commentary: +;; + +;;; Code: + (let ((version (getenv "PROOFGENERAL"))) (cond ((not version) ;default (setq load-path @@ -20,4 +34,4 @@ (load-file "/usr/local/share/elisp/ProofGeneral/generic/proof-site.el")))) -
\ No newline at end of file + diff --git a/etc/testsuite/pg-pgip-test.el b/etc/testsuite/pg-pgip-test.el index 9dbfaad7..968c2289 100644 --- a/etc/testsuite/pg-pgip-test.el +++ b/etc/testsuite/pg-pgip-test.el @@ -1,6 +1,18 @@ -;; Tests for pg-pgip.el +;;; Tests for pg-pgip.el + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: ;; -;; $Id$ + +;;; Code: (pg-clear-test-suite "pg-pgip") (pg-set-test-suite "pg-pgip") @@ -13,4 +25,4 @@ (provide 'pg-pgip-test) -;; End of `pg-pgip-test.el'
\ No newline at end of file +;; End of `pg-pgip-test.el' diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el index b8d236a7..2e3c2c10 100644 --- a/etc/testsuite/pg-test.el +++ b/etc/testsuite/pg-test.el @@ -1,8 +1,19 @@ -;; pg-test.el -- Simple test framework for Proof General. -;; -;; $Id$ +;;; pg-test.el --- Simple test framework for Proof General. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: ;; +;;; Code: + (defconst pg-test-buffer "** PG test output **") (defvar pg-test-total-success-count 0) diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index a8a52099..714429b7 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -1,12 +1,19 @@ ;;; pg-assoc.el --- Functions for associated buffers -;; -;; Copyright (C) 1994-2008, 2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Defines an empty mode inherited by modes of the associated buffers. diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index 8dfee09d..bc3ab9c5 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -1,10 +1,18 @@ ;;; pg-autotest.el --- Simple testing framework for Proof General -;; -;; Copyright (C) 2005, 2009-11 LFCS Edinburgh, David Aspinall. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall -;; + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; + ;;; Commentary: ;; ;; Support for running a series of scripted UI tests. @@ -14,8 +22,8 @@ ;; -- add macros for defining test suites ;; -- add more precise functional tests to check results ;; -- add negative tests -;; -;; $Id$ + +;;; Code: (require 'proof-splash) (setq proof-splash-enable nil) ; prevent splash when testing diff --git a/generic/pg-custom.el b/generic/pg-custom.el index 0956f970..8a7bb793 100644 --- a/generic/pg-custom.el +++ b/generic/pg-custom.el @@ -1,11 +1,18 @@ ;;; pg-custom.el --- Proof General per-prover settings -;; -;; Copyright (C) 2008, 2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Prover specific settings and user options. diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 5270ae3d..c35f0f29 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -1,12 +1,18 @@ -;; pg-goals.el --- Proof General goals buffer mode. -;; -;; Copyright (C) 1994-2009 LFCS, University of Edinburgh. +;;; pg-goals.el --- Proof General goals buffer mode. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; ;;; Commentary: diff --git a/generic/pg-movie.el b/generic/pg-movie.el index 03ea5497..ba641c20 100644 --- a/generic/pg-movie.el +++ b/generic/pg-movie.el @@ -1,11 +1,18 @@ ;;; pg-movie.el --- Export a processed script buffer for external replay -;; -;; Copyright (C) 2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Given a processed proof script, write out an XML file that diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index d7bb1bf3..9792dfd0 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -1,8 +1,16 @@ ;;; pg-pamacs.el --- Macros for per-proof assistant configuration -;; -;; Copyright (C) 2010, 2011 LFCS Edinburgh, David Aspinall. -;; + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <da@longitude> + ;; Keywords: internal ;;; Commentary: @@ -24,14 +32,13 @@ ;; ;; (proof-ass name) or (proof-assistant-name) ;; -;; + +;;; Code: (require 'proof-site) ; proof-assitant-symbol (require 'proof-compat) ; pg-custom-undeclare-variable (require 'proof-autoloads) ; proof-debug -;;; Code: - (defmacro deflocal (var value &optional docstring) "Define a buffer local variable VAR with default value VALUE." `(progn diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index cd9dac2a..997f8bb1 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -1,10 +1,19 @@ -;; pg-pgip.el --- PGIP manipulation for Proof General -;; -;; Copyright (C) 2000-2002, 2010 LFCS Edinburgh. +;;; pg-pgip.el --- PGIP manipulation for Proof General + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; ;; STATUS: Experimental ;; @@ -23,10 +32,7 @@ ;; -- support fully native PGIP mode ;; - -;;; Commentary: -;; - +;;; Code: (require 'cl) ; incf (require 'pg-xml) ; @@ -35,7 +41,6 @@ (declare-function proof-segment-up-to "proof-script") (declare-function proof-insert-pbp-command "proof-script") -;;; Code: (defalias 'pg-pgip-debug 'proof-debug) (defalias 'pg-pgip-error 'error) (defalias 'pg-pgip-warning 'pg-internal-warning) diff --git a/generic/pg-response.el b/generic/pg-response.el index 8b6a413a..d89d3c0b 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -1,12 +1,19 @@ -;; pg-response.el --- Proof General response buffer mode. -;; -;; Copyright (C) 1994-2010 LFCS Edinburgh. +;;; pg-response.el --- Proof General response buffer mode. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; pg-response.el,v 12.10 2012/09/25 09:44:18 pier Exp -;; + ;;; Commentary: ;; ;; This mode is used for the response buffer proper, and diff --git a/generic/pg-user.el b/generic/pg-user.el index 11a731fb..21d9479d 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1,13 +1,18 @@ ;;; pg-user.el --- User level commands for Proof General -;; -;; Copyright (C) 2000-2010 LFCS Edinburgh. -;; Copyright (c) 2010 Erik Martin-Dorel, ENS de Lyon (pg-protected-undo). + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; -;; + ;;; Commentary: ;; ;; This file defines some user-level commands. Most of them diff --git a/generic/pg-vars.el b/generic/pg-vars.el index 8d93a60b..546c955e 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -1,11 +1,18 @@ ;;; pg-vars.el --- Proof General global variables -;; -;; Copyright (C) 2008, 2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Global variables used in several files. diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 79d15b55..5de8095d 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -1,14 +1,25 @@ -;; pg-xml.el --- XML functions for Proof General -;; -;; Copyright (C) 2000-2002 LFCS Edinburgh. +;;; pg-xml.el --- XML functions for Proof General + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; ;; XML functions for Proof General. ;; +;;; Code: + (require 'cl) (require 'xml) diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 67287511..5cd83ddd 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -1,5 +1,17 @@ ;;; proof-autoloads.el --- automatically extracted autoloads + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: ;; + ;;; Code: (if (featurep 'proof-autoloads) (error "Already loaded")) diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el index aa6ddd23..d3ccf41e 100644 --- a/generic/proof-auxmodes.el +++ b/generic/proof-auxmodes.el @@ -1,7 +1,16 @@ ;;; proof-auxmodes.el --- Arrange for auxiliary modes to be loaded when required -;; -;; Copyright (C) 2008, 2010 David Aspinall / LFCS Edinburgh + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: @@ -10,10 +19,10 @@ ;; loading of their main defining files and the possibility to disable them. ;; -(require 'proof-utils) ; proof-ass, proof-eval... - ;;; Code: +(require 'proof-utils) ; proof-ass, proof-eval... + ;; ;; Maths menu ;; diff --git a/generic/proof-config.el b/generic/proof-config.el index 8bb40634..bd5ca611 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1,11 +1,18 @@ ;;; proof-config.el --- Proof General configuration for proof assistant -;; -;; Copyright (C) 1998-2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; This file declares all prover-specific configuration variables for diff --git a/generic/proof-depends.el b/generic/proof-depends.el index c55df53d..74332c71 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,21 +1,28 @@ ;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies -;; -;; Copyright (C) 2000-2004, 2010 University of Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Earlier version by Fiona McNeil. + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Status: Experimental code + +;;; Commentary: ;; -;; $Id$ +;; Status: Experimental code ;; -;;; Commentary: -;; ;; Based on Fiona McNeill's MSc project on analysing dependencies ;; within proofs. Code rewritten by David Aspinall. ;; - - +;;; Code: (require 'cl) (require 'span) (require 'pg-vars) @@ -34,9 +41,6 @@ A list of lists; the first element of each list is a file-name, the second element a list of all the def names in that file. i.e.: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))") - -;;; Code: - ;; Utility functions (defun proof-depends-module-name-for-buffer () diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index da3b9c7f..59fa03e5 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -1,16 +1,27 @@ -;; proof-easy-config.el Easy configuration for Proof General -;; -;; Copyright (C) 1999-2002 David Aspinall / LFCS. +;;; proof-easy-config.el --- Easy configuration for Proof General + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; ;; Future versions might copy settings instead; consider how best to ;; interface with customization mechanism so a new prover can be ;; configured by editing inside custom buffers. ;; +;;; Code: + (require 'proof-site) ; proof-assistant, proof-assistant-symbol (require 'proof-auxmodes) ; make sure extra modes available diff --git a/generic/proof-faces.el b/generic/proof-faces.el index 0eafc075..92609d47 100644 --- a/generic/proof-faces.el +++ b/generic/proof-faces.el @@ -1,11 +1,18 @@ ;;; proof-faces.el --- Faces for Proof General -;; -;; Copyright (C) 2009 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; In an ideal world, faces should work sensibly: diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 2ff6cf69..24da2059 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -1,21 +1,27 @@ ;;; proof-indent.el --- Generic indentation for proof assistants -;; + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Markus Wenzel, David Aspinall -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; +;;; Code: (require 'proof-config) ; config variables (require 'proof-utils) ; proof-ass (require 'proof-syntax) ; p-looking-at-safe, p-re-search (require 'proof-autoloads) ; p-locked-end -;;; Code: (defun proof-indent-indent () "Determine indentation caused by syntax element at current point." (cond diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el index 57fafa98..b1155557 100644 --- a/generic/proof-maths-menu.el +++ b/generic/proof-maths-menu.el @@ -1,16 +1,22 @@ ;;; proof-maths-menu.el --- Support for maths menu mode package -;; -;; Copyright (C) 2007, 2009 LFCS Edinburgh / David Aspinall + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; + +;;; Commentary: ;; ;; With thanks to Dave Love for the original maths menu code, ;; provided at http://www.loveshack.ukfsn.org/emacs/ -;; -;; $Id$ -;; -;;; Commentary: ;; ;; Note: maths menu is bundled with Proof General in lib/, and PG will select ;; it's own version before any other version on the Emacs load path. diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 0a7317cb..f893a9f6 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -1,15 +1,24 @@ ;;; proof-menu.el --- Menus, keymaps, misc commands for Proof General -;; -;; Copyright (C) 2000,2001,2009,2010,2011 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; +;;; Code: (require 'cl) ; mapcan -;;; Code: (eval-when-compile (defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific (defvar proof-mode-map)) @@ -113,6 +122,7 @@ without adjusting window layout." ;; C-c C-v is proof-minibuffer-cmd in universal-keys ;; C-c C-. is proof-goto-end-of-locked in universal-keys (define-key map [(control c) (control return)] 'proof-goto-point) + (define-key map [(control c) (control m)] 'proof-goto-point) ; fallback for tty (define-key map [(control c) ?v] 'pg-toggle-visibility) (define-key map [(control meta mouse-3)] 'proof-mouse-goto-point) ;; NB: next binding overwrites comint-find-source-code. diff --git a/generic/proof-script.el b/generic/proof-script.el index eb8fac7a..0baf3d5f 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1,12 +1,19 @@ ;;; proof-script.el --- Major mode for proof assistant script files. -;; -;; Copyright (C) 1994-2010 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; This implements the main mode for script management, including diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 6f3180fe..00d8b1d7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1,12 +1,19 @@ ;;; proof-shell.el --- Proof General shell mode. -;; -;; Copyright (C) 1994-2011 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Mode for buffer which interacts with proof assistant. diff --git a/generic/proof-site.el b/generic/proof-site.el index 70a517b2..dccc32a9 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -1,11 +1,18 @@ -;; proof-site.el -- Loading stubs for Proof General. -;; -;; Copyright (C) 1998-2003 LFCS Edinburgh. +;;; proof-site.el --- Loading stubs for Proof General. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Loading stubs and configuration for site and choice of provers. diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 7e7b8d54..daa09eff 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -1,12 +1,18 @@ -;; proof-splash.el -- Splash welcome screen for Proof General -;; -;; Copyright (C) 1998-2005, 2009, 2010 LFCS Edinburgh. +;;; proof-splash.el --- Splash welcome screen for Proof General + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; -;; + ;;; Commentary: ;; ;; Provide splash screen for Proof General. diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 84b5940d..7af4dd06 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -1,23 +1,27 @@ -;; proof-syntax.el --- Functions for dealing with syntax -;; -;; Copyright (C) 1997-2001, 2010 LFCS Edinburgh. +;;; proof-syntax.el --- Functions for dealing with syntax + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Healfdene Goguen, ;; Thomas Kleymann, Dilip Sequiera -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; - -(require 'font-lock) -(require 'proof-config) ; proof-case-fold-search -(require 'proof-compat) ; proof-buffer-syntactic-context -(require 'pg-pamacs) ; proof-ass-sym +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; ;;; Code: +(require 'font-lock) +(require 'proof-config) ; proof-case-fold-search +(require 'proof-compat) ; proof-buffer-syntactic-context +(require 'pg-pamacs) ; proof-ass-sym (defsubst proof-ids-to-regexp (l) "Maps a non-empty list of tokens L to a regexp matching any element. @@ -232,7 +236,7 @@ this were even more bogus...." (eval-after-load "font-lock" '(progn (defadvice font-lock-fontify-keywords-region - (before font-lock-fontify-keywords-advice (beg end loudly)) + (before font-lock-fontify-keywords-advice (beg end &optional loudly)) "Call proof assistant specific syntactic region fontify. If it's bound, we call <PA>-font-lock-fontify-syntactically-region." (when (and proof-buffer-type diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index af9e8694..88552476 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -1,11 +1,18 @@ ;;; proof-toolbar.el --- Toolbar for Proof General -;; -;; Copyright (C) 1998-2009 David Aspinall / LFCS. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; It's a little bit tricky to add prover-specific items: diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 438c035e..996934b6 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -1,11 +1,18 @@ ;;; tree-tree.el --- Proof General prooftree communication. -;; -;; Copyright (C) 2012 Hendrik Tews + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Generic code for the communication with prooftree. Prooftree diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el index 0352f012..2deca0e6 100644 --- a/generic/proof-unicode-tokens.el +++ b/generic/proof-unicode-tokens.el @@ -1,12 +1,18 @@ ;;; proof-unicode-tokens.el --- Support Unicode tokens package -;; -;; Copyright (C) 2008, 2009 David Aspinall / LFCS Edinburgh + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; -;; + ;;; Commentary: ;; ;; Support for Unicode Tokens package: per-prover global enabling, copying diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index eb9942a7..b1d8e2e4 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -1,11 +1,18 @@ ;;; proof-useropts.el --- Global user options for Proof General -;; -;; Copyright (C) 2009, 2010, 2011 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; User options for Proof General. diff --git a/generic/proof-utils.el b/generic/proof-utils.el index dff19e76..575a76ee 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -1,11 +1,18 @@ -;; proof-utils.el --- Proof General utility functions and macros -;; -;; Copyright (C) 1998-2002, 2009, 2011 LFCS Edinburgh. +;;; proof-utils.el --- Proof General utility functions and macros + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Loading note: this file is required immediately from proof.el, so diff --git a/generic/proof.el b/generic/proof.el index 4e7ddbea..5fa9de33 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -1,14 +1,21 @@ ;;; proof.el --- Proof General theorem prover interface. -;; -;; Copyright (C) 1998-2009 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; + ;; Keywords: languages -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; This file loads Proof General. It is required by the diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el index 5c1cb011..d68b898f 100644 --- a/hol-light/hol-light-autotest.el +++ b/hol-light/hol-light-autotest.el @@ -1,9 +1,20 @@ -;; hol-light-autotest.el: tests of HOL Light Proof General. +;;; hol-light-autotest.el --- tests of HOL Light Proof General. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;;; Commentary: ;; ;; You can run these by issuing "make test.hol-light" in PG home dir. ;; -;; $Id$ -;; + +;;; Code: (eval-when-compile (require 'cl)) diff --git a/hol-light/hol-light-unicode-tokens.el b/hol-light/hol-light-unicode-tokens.el index df32e4bd..7e24e4b1 100644 --- a/hol-light/hol-light-unicode-tokens.el +++ b/hol-light/hol-light-unicode-tokens.el @@ -1,8 +1,17 @@ -;;; -*- coding: utf-8; -*- -;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -;; -;; Copyright(C) 2012 David Aspinall / University of Edinburgh +;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*- + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + +;;; Commentary: ;; ;; This file is loaded by `proof-unicode-tokens.el'. ;; @@ -18,6 +27,8 @@ ;; - fix unicode tokens sorting so longs tokens handled first (broken?) ;; <=> not <= > +;;; Code: + (require 'proof-unicode-tokens) (defconst hol-light-token-format "%s") ; plain tokens diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 467453ed..2b4f3989 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -1,15 +1,24 @@ -;; hol-light.el Basic Proof General instance for HOL Light -;; -;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall. -;; +;;; hol-light.el --- Basic Proof General instance for HOL Light + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; Mark Adams <mark@proof-technologies.com> -;; -;; $Id$ + +;;; Commentary: ;; ;; See the README file in this directory for information. ;; +;;; Code: + (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps diff --git a/hol98/hol98.el b/hol98/hol98.el index a96da637..6f89707b 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -1,15 +1,22 @@ -;; hol98.el Basic Proof General instance for HOL 98 -;; -;; Copyright (C) 2000 LFCS Edinburgh. -;; +;;; hol98.el --- Basic Proof General instance for HOL 98 + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> -;; -;; $Id$ -;; + +;;; Commentary: ;; Needs improvement! ;; ;; See the README file in this directory for information. +;;; Code: (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 44a17ade..1cca4cf2 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -1,12 +1,23 @@ -;; lego-syntax.el Syntax of LEGO -;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;;; lego-syntax.el --- Syntax of LEGO + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: Thomas Kleymann and Dilip Sequeira -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: ;; -;; $Id$ -;; + +;;; Code: (require 'proof-syntax) diff --git a/lego/lego.el b/lego/lego.el index d1bd7532..29564c87 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -1,12 +1,23 @@ -;; lego.el Major mode for LEGO proof assistants -;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;;; lego.el --- Major mode for LEGO proof assistants + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: Thomas Kleymann and Dilip Sequeira -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: ;; -;; $Id$ -;; + +;;; Code: (require 'proof) (require 'lego-syntax) diff --git a/lib/bufhist.el b/lib/bufhist.el index 3d6a123d..4c24ca42 100644 --- a/lib/bufhist.el +++ b/lib/bufhist.el @@ -1,16 +1,24 @@ ;; bufhist.el --- keep read-only history of buffer contents for browsing -;; Copyright (C) 2006, 2009 David Aspinall / University of Edinburgh +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Keywords: tools -;; -;; $Id$ -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + ;; This file is distributed under the terms of the GNU General Public ;; License, Version 2. Find a copy of the GPL with your version of ;; GNU Emacs or Texinfo. + +;;; Commentary: ;; ;; This library implements a minor mode for which keeps a ring history of ;; buffer contents. Intended to be used for small buffers which are @@ -29,6 +37,8 @@ ;; - buttons are put at top of buffer but inserts happen before them ;; +;;; Code: + (require 'ring) (declare-function bufhist-ordinary-erase-buffer "bufhist") diff --git a/lib/holes.el b/lib/holes.el index 38a90cfb..2b154723 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -1,9 +1,14 @@ ;;; holes.el --- a little piece of elisp to define holes in your buffer -;; -;; Copyright (C) 2001 Pierre Courtieu -;; -;; $Id$ -;; + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; This file uses spans, an interface for extent (XEmacs) and overlays ;; (emacs), by Healfdene Goguen for the proofgeneral mode. ;; @@ -11,7 +16,7 @@ ;; cleaner. ;; ;; Further cleanups by David Aspinall. -;; + ;; This software is free software; you can redistribute it and/or ;; modify it under the terms of the GNU General Public ;; License version 2, as published by the Free Software Foundation. @@ -22,19 +27,17 @@ ;; ;; See the GNU General Public License version 2 for more details ;; (enclosed in the file GPL). -;; -;; See documentation in variable holes-short-doc. -;; ;;; Commentary: ;; +;; See documentation in variable holes-short-doc. +;; ;; See documentation of `holes-mode'. +;;; Code: (require 'span) (require 'cl) -;;; Code: - ;;; ;;; initialization ;;; diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index 3fa0103d..bcea270f 100644 --- a/lib/local-vars-list.el +++ b/lib/local-vars-list.el @@ -1,10 +1,16 @@ ;;; local-vars.el --- local variables list utilities -;; -;; Copyright (C) 2006 Pierre Courtieu + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Pierre Courtieu ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; -;; $Id$ ;; This software is free software; you can redistribute it and/or ;; modify it under the terms of the GNU General Public @@ -18,14 +24,12 @@ ;; (enclosed in the file GPL). ;;; Commentary: +;; ;; See documentation in variable local-var-list-doc - -;;; TODO: Rely on hack-file-local-variables instead - -;;; History: ;; +;; TODO: Rely on hack-file-local-variables instead -;;; Help: +;;; Code: (defconst local-vars-list-doc nil "From Emacs Info: diff --git a/lib/maths-menu.el b/lib/maths-menu.el index b9ddf927..a6b64201 100644 --- a/lib/maths-menu.el +++ b/lib/maths-menu.el @@ -1,16 +1,20 @@ ;;; maths-menu.el --- insert maths characters from a menu -*-coding: iso-2022-7bit;-*- -;; Copyright (C) 2003, 2012 Free Software Foundation, Inc. +;; This file is part of Proof General. + +;; Portions ,A)(B Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions ,A)(B Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions ,A)(B Copyright 2001-2017 Pierre Courtieu +;; Portions ,A)(B Copyright 2010, 2016 Erik Martin-Dorel +;; Portions ,A)(B Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions ,A)(B Copyright 2015-2017 Cl,Ai(Bment Pit-Claudel ;; Author: Dave Love <fx@gnu.org> ;; Keywords: convenience - ;; Version for Proof General modified by David Aspinall, 2007-8. ;; - Hooks added to insert tokenised versions of unicode characters. ;; - Added more characters to the menus. ;; - Define insertion functions following menu names (useful for keybindings) -;; $Id$ - ;; This file is free software; you can redistribute it and/or modify ;; it under the terms of the GNU General Public License as published by @@ -49,8 +53,6 @@ ;; the minibuffer via the menu, though presumably it could be added to ;; the minibuffer menu. - - ;;; Code: (defvar maths-menu-filter-predicate (lambda (char) t) diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 758b3d51..79afca23 100644 --- a/lib/pg-dev.el +++ b/lib/pg-dev.el @@ -1,11 +1,18 @@ ;;; pg-dev.el --- Developer settings for Proof General -;; -;; Copyright (C) 2008-2011 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ - ;; + ;;; Commentary: ;; ;; Some configuration of Emacs Lisp mode for developing PG, not needed diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el index c4d76efc..771e76f1 100644 --- a/lib/pg-fontsets.el +++ b/lib/pg-fontsets.el @@ -1,11 +1,18 @@ ;;; pg-fontsets.el --- Define fontsets useful for Proof General -;; -;; Copyright (C) 2008 David Aspinall / LFCS Edinburgh + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Define some fontsets to try to select fonts that display many symbols. diff --git a/lib/proof-compat.el b/lib/proof-compat.el index 4eb942cb..4c1fa5b2 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -1,10 +1,19 @@ -;; proof-compat.el Operating system and Emacs version compatibility -;; -;; Copyright (C) 2000-2010 LFCS Edinburgh. +;;; proof-compat.el --- Operating system and Emacs version compatibility + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; ;; This file collects together compatibility hacks for different ;; operating systems and Emacs versions. This is to help keep @@ -17,6 +26,8 @@ ;; Since Proof General 4.0, XEmacs is not supported at all. ;; +;;; Code: + (require 'easymenu) (require 'cl) diff --git a/lib/scomint.el b/lib/scomint.el index af8df997..3644add2 100644 --- a/lib/scomint.el +++ b/lib/scomint.el @@ -1,10 +1,17 @@ ;;; scomint.el --- Simplified comint for less interactive shells -;; -;; Copyright (C) 2009 LFCS Edinburgh. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ ;;; Commentary: ;; @@ -16,6 +23,8 @@ ;; hard to disentangle. ;; +;;; Code: + (defvar scomint-buffer-maximum-size 800000 "The maximum size in characters for SComint buffers. SComint buffers are truncated from the top to be no greater than this number, diff --git a/lib/span.el b/lib/span.el index f1379616..2252d605 100644 --- a/lib/span.el +++ b/lib/span.el @@ -1,12 +1,19 @@ ;;; span.el --- Datatype of "spans" for Proof General -;; -;; Copyright (C) 1998-2009 LFCS Edinburgh + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: Healfdene Goguen ;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;;; Commentary: ;; ;; Spans are our abstraction of extents/overlays. Nowadays @@ -16,6 +23,7 @@ ;; ;;; Code: + (eval-when-compile (require 'cl)) ;For lexical-let. (defalias 'span-start 'overlay-start) diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el index 6e8c8e49..93896209 100644 --- a/lib/texi-docstring-magic.el +++ b/lib/texi-docstring-magic.el @@ -1,16 +1,24 @@ -;; texi-docstring-magic.el --- munge internal docstrings into texi -;; -;; Keywords: lisp, docs, tex +;;; texi-docstring-magic.el --- munge internal docstrings into texi + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> -;; Copyright (C) 1998 David Aspinall +;; Keywords: lisp, docs, tex + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;; This file is distributed under the terms of the GNU General Public ;; License, Version 2. Find a copy of the GPL with your version of ;; GNU Emacs or Texinfo. -;; + +;;; Commentary: ;; ;; This package generates Texinfo source fragments from Emacs ;; docstrings. This avoids documenting functions and variables in @@ -82,6 +90,8 @@ ;; ;; +;;; Code: + (eval-when-compile (require 'cl)) diff --git a/lib/unicode-chars.el b/lib/unicode-chars.el index 1e5dedbf..880371ce 100644 --- a/lib/unicode-chars.el +++ b/lib/unicode-chars.el @@ -1,7 +1,17 @@ -;; unicode-chars.el --- table of Unicode characters -;; +;;; unicode-chars.el --- table of Unicode characters + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall -;; $Id$ + +;;; Commentary: ;; ;; Adapted from Norman Walsh's unichars.el (iso8879 names removed) ;; @@ -9,6 +19,8 @@ ;; http://www.unicode.org/unicode/standard/standard.html ;; http://www.unicode.org/Public/UNIDATA +;;; Code: + (defvar unicode-chars-alist '(;Unicode name Codept ("NULL" . #x000000) diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index d05bfc1e..e98ca0a2 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -1,11 +1,18 @@ ;;; unicode-tokens.el --- Support for control and symbol tokens -;; -;; Copyright(C) 2008-2010 David Aspinall / LFCS Edinburgh + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; + ;; This is free software; you can redistribute it and/or modify ;; it under the terms of the GNU General Public License as published by ;; the Free Software Foundation; either version 2, or (at your option) @@ -37,9 +44,7 @@ ;; -- simplify/optimise property handling ;; -- support multiple modes with mode-local configs at once -;; ;;; Code: -;; (require 'cl) (require 'quail) @@ -1,6 +1,13 @@ ;;; pg-init.el --- Init file used for compatibility with package.el and ELPA -*- lexical-binding: t; -*- -;; Copyright (C) 2017 Clément Pit-Claudel +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Author: Clément Pit-Claudel <clement.pitclaudel@live.com> @@ -18,7 +25,7 @@ ;; along with this program. If not, see <http://www.gnu.org/licenses/>. ;;; Commentary: - +;; ;; Proof General's initialization code (in generic/proof-site) is relatively ;; complex, in part because it was written before package.el existed, and in ;; part because package.el still doesn't look for autoloads in subdirectories. diff --git a/pghaskell/pghaskell.el b/pghaskell/pghaskell.el index f2aec426..7784cf0f 100644 --- a/pghaskell/pghaskell.el +++ b/pghaskell/pghaskell.el @@ -1,6 +1,17 @@ -;; pghaskell.el - Proof General for Haskell scripts. -;; -;; David Aspinall. $Id$ +;;; pghaskell.el --- Proof General for Haskell scripts. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;; Author: David Aspinall. + +;;; Commentary: ;; ;; This instance of PG is handy just for using script management to ;; cut-and-paste into a buffer running Haskell (ghci) @@ -18,6 +29,7 @@ ;; in proof-site.el). ;; +;;; Code: (require 'proof-easy-config) (require 'proof-syntax) diff --git a/pgocaml/pgocaml.el b/pgocaml/pgocaml.el index 4b11c7df..dcf179d0 100644 --- a/pgocaml/pgocaml.el +++ b/pgocaml/pgocaml.el @@ -1,6 +1,17 @@ -;; pgocaml.el - Proof General for OCaml scripts. -;; -;; David Aspinall. $Id$ +;;; pgocaml.el --- Proof General for OCaml scripts. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;; Author: David Aspinall + +;;; Commentary: ;; ;; This instance of PG is handy just for using script management to ;; cut-and-paste into a buffer running OCaml @@ -18,6 +29,7 @@ ;; in proof-site.el). ;; +;;; Code: (require 'proof-easy-config) (require 'proof-syntax) diff --git a/pgshell/pgshell.el b/pgshell/pgshell.el index aa34e985..39c780dc 100644 --- a/pgshell/pgshell.el +++ b/pgshell/pgshell.el @@ -1,6 +1,17 @@ -;; pgshell.el - Proof General for shell scripts. -;; -;; David Aspinall. $Id$ +;;; pgshell.el --- Proof General for shell scripts. + +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;; Author: David Aspinall. + +;;; Commentary: ;; ;; This instance of PG is handy just for using script management to ;; cut-and-paste into a buffer running an ordinary shell of some kind. @@ -13,6 +24,7 @@ ;; ;; Feedback welcome. +;;; Code: (require 'proof-easy-config) (require 'proof-syntax) diff --git a/twelf/twelf-old.el b/twelf/twelf-old.el index 41664839..62763ba4 100644 --- a/twelf/twelf-old.el +++ b/twelf/twelf-old.el @@ -2535,38 +2535,38 @@ Mode map (setq twelf-server-display-commands (not twelf-server-display-commands))) (defconst twelf-options-menu - (` ("Options" - (, (toggle "Display Commands" '(twelf-toggle-server-display-commands) - 'twelf-server-display-commands)) - ("chatter" - (, (radio "0" '(twelf-set "chatter" 0) '(= twelf-chatter 0))) - (, (radio "1" '(twelf-set "chatter" 1) '(= twelf-chatter 1))) - (, (radio "2" '(twelf-set "chatter" 2) '(= twelf-chatter 2))) - (, (radio "3*" '(twelf-set "chatter" 3) '(= twelf-chatter 3))) - (, (radio "4" '(twelf-set "chatter" 4) '(= twelf-chatter 4))) - (, (radio "5" '(twelf-set "chatter" 5) '(= twelf-chatter 5))) - (, (radio "6" '(twelf-set "chatter" 6) '(= twelf-chatter 6)))) - (, (toggle "doubleCheck" '(twelf-toggle-double-check) - '(string-equal twelf-double-check "true"))) - ("Print." - (, (toggle "implicit" '(twelf-toggle-print-implicit) - '(string-equal twelf-print-implicit "true"))) - ["depth" (twelf-set-parm "Print.depth") t] - ["length" (twelf-set-parm "Print.length") t] - ["indent" (twelf-set-parm "Print.indent") t] - ["width" (twelf-set-parm "Print.width") t]) - ("Prover." - ["strategy" (twelf-set-parm "Prover.strategy") t] - ["maxSplit" (twelf-set-parm "Prover.maxSplit") t] - ["maxRecurse" (twelf-set-parm "Prover.maxRecurse") t]) - ;;["Trace" nil nil] - ;; (, (radio "0" '(twelf-set "trace" 0) '(= twelf-trace 0))) - ;; (, (radio "1" '(twelf-set "trace 1) '(= twelf-trace 1))) - ;; (, (radio "2" '(twelf-set "trace" 2) '(= twelf-trace 2)))) - ;;["Untrace" nil nil] - ;;(, (disable-form "Untrace" '(twelf-set "trace" 0) - ;; '(not (= twelf-trace 0)))) - ["Reset Menubar" twelf-reset-menu t])) + `("Options" + (, (toggle "Display Commands" '(twelf-toggle-server-display-commands) + 'twelf-server-display-commands)) + ("chatter" + (, (radio "0" '(twelf-set "chatter" 0) '(= twelf-chatter 0))) + (, (radio "1" '(twelf-set "chatter" 1) '(= twelf-chatter 1))) + (, (radio "2" '(twelf-set "chatter" 2) '(= twelf-chatter 2))) + (, (radio "3*" '(twelf-set "chatter" 3) '(= twelf-chatter 3))) + (, (radio "4" '(twelf-set "chatter" 4) '(= twelf-chatter 4))) + (, (radio "5" '(twelf-set "chatter" 5) '(= twelf-chatter 5))) + (, (radio "6" '(twelf-set "chatter" 6) '(= twelf-chatter 6)))) + (, (toggle "doubleCheck" '(twelf-toggle-double-check) + '(string-equal twelf-double-check "true"))) + ("Print." + (, (toggle "implicit" '(twelf-toggle-print-implicit) + '(string-equal twelf-print-implicit "true"))) + ["depth" (twelf-set-parm "Print.depth") t] + ["length" (twelf-set-parm "Print.length") t] + ["indent" (twelf-set-parm "Print.indent") t] + ["width" (twelf-set-parm "Print.width") t]) + ("Prover." + ["strategy" (twelf-set-parm "Prover.strategy") t] + ["maxSplit" (twelf-set-parm "Prover.maxSplit") t] + ["maxRecurse" (twelf-set-parm "Prover.maxRecurse") t]) + ;;["Trace" nil nil] + ;; (, (radio "0" '(twelf-set "trace" 0) '(= twelf-trace 0))) + ;; (, (radio "1" '(twelf-set "trace 1) '(= twelf-trace 1))) + ;; (, (radio "2" '(twelf-set "trace" 2) '(= twelf-trace 2)))) + ;;["Untrace" nil nil] + ;;(, (disable-form "Untrace" '(twelf-set "trace" 0) + ;; '(not (= twelf-trace 0)))) + ["Reset Menubar" twelf-reset-menu t]) "Menu to change options in Twelf mode.") (defconst twelf-timers-menu @@ -2583,12 +2583,12 @@ Mode map "Fontify current buffer using font-lock minor mode.") (defconst twelf-syntax-menu - (` ("Syntax Highlighting" - ["Highlight Declaration" twelf-font-fontify-decl t] - ["Highlight Buffer" twelf-font-fontify-buffer t] - ;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate - ;'font-lock-mode)) - )) + `("Syntax Highlighting" + ["Highlight Declaration" twelf-font-fontify-decl t] + ["Highlight Buffer" twelf-font-fontify-buffer t] + ;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate + ;;'font-lock-mode)) + ) "Menu for syntax highlighting in Twelf mode.") (easy-menu-define twelf-menu (list twelf-mode-map) |