1 files changed, 18 insertions, 9 deletions
diff --git a/lib/span.el b/lib/span.el
index f1379616..e7e3d68b 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)
@@ -31,7 +39,7 @@
 (defalias 'span-buffer 'overlay-buffer)
 
 (defun span-p (ol)
-  "Check if an overlay belongs to PG."
+  "Check if an overlay OL belongs to PG."
   (overlay-get ol 'pg-span))
 
 (defun span-read-only-hook (overlay after start end &optional len)
@@ -111,7 +119,7 @@
 
 (defun span-mapcar-spans-inorder (fn start end prop)
   "Map function FN over spans between START and END with property PROP."
-  (mapcar fn 
+  (mapcar fn
 	  (sort (spans-at-region-prop start end prop)
 		'span-lt)))
 
@@ -157,7 +165,7 @@ A span is before PT if it begins before the character before PT."
 
 (defun span-string (span)
   (with-current-buffer (overlay-buffer span)
-    (buffer-substring-no-properties 
+    (buffer-substring-no-properties
      (overlay-start span) (overlay-end span))))
 
 (defun set-span-properties (span plist)
@@ -204,7 +212,8 @@ A span is before PT if it begins before the character before PT."
   (span-mapc-spans 'span-delete start end prop))
 
 (defun span-property-safe (span name)
-  "Like span-property, but return nil if SPAN is nil."
+  "Get the property of span SPAN with property name NAME.
+Like ‘span-property’, but return nil if SPAN is nil."
   (and span (span-property span name)))
 
 (defun span-set-start (span value)