diff options
78 files changed, 1182 insertions, 460 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,21 @@ 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. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some 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 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..dd9020d8 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) 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..2b5e59e9 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 @@ -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..63d44666 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 @@ -516,7 +529,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 diff --git a/coq/coq-system.el b/coq/coq-system.el index 0bcf6a07..f3eabafc 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 @@ -32,7 +43,7 @@ (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) @@ -416,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 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) @@ -78,7 +89,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 +102,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 +443,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 +896,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 @@ -1840,7 +1852,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) 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 df17229d..c7d721cd 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) |