Update copyright messages and improve the header of elisp files.

12 files changed, 161 insertions, 73 deletions

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)