Update copyright messages and improve the header of elisp files.

31 files changed, 402 insertions, 182 deletions

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 35c6eb3b..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))
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..cba709d9 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.
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