Rework headers; add missing copyright notice

leanprover-community · Nov 27, 2024 · c30b676 · c30b676
1 parent a9eab22
commit c30b676
Show file tree

Hide file tree

Showing 11 changed files with 104 additions and 148 deletions.
diff --git a/lean4-debug.el b/lean4-debug.el
@@ -1,25 +1,20 @@
-;;; lean4-debug.el --- Debug mode for lean4-mode -*- lexical-binding: t -*-
+;;; lean4-debug.el --- Lean4-Mode Debug Mode  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 
-;; Author: Soonho Kong
-;; SPDX-License-Identifier: Apache-2.0
-
 ;; This file is not part of GNU Emacs.
 
-;;; License:
-
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-dev.el b/lean4-dev.el
@@ -1,25 +1,20 @@
-;;; lean4-dev.el --- Development commands for lean4-mode -*- lexical-binding: t -*-
+;;; lean4-dev.el --- Lean4-Mode Development Commands  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 
-;; Author: Sebastian Ullrich
-;; SPDX-License-Identifier: Apache-2.0
-
 ;; This file is not part of GNU Emacs.
 
-;;; License:
-
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-eri.el b/lean4-eri.el
@@ -1,24 +1,27 @@
-;;; lean4-eri.el --- Enhanced relative indentation (eri) -*- lexical-binding: t -*-
+;;; lean4-eri.el --- Lean4-Mode Indentation  -*- lexical-binding: t; -*-
 
-;; SPDX-License-Identifier: Apache-2.0
+;; Copyright (c) 2005-2010 Ulf Norell, Nils Anders Danielsson,
+;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter,
+;; Marcin Benke, Darin Morrison.
 
-;;; License:
+;; This file is not part of GNU Emacs.
 
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 
-;; Adapted from agda-mode (https://github.com/agda/agda/blob/master/src/data/emacs-mode/eri.el)
+;; Adapted from Agda-Mode:
+;; https://github.com/agda/agda/blob/b40c6fc2e0ced7b547553654f81e5898082d700c/src/data/emacs-mode/eri.el
 
 ;;; Code:
 

diff --git a/lean4-fringe.el b/lean4-fringe.el
@@ -1,29 +1,25 @@
-;;; lean4-fringe.el --- Show Lean processing progress in the editor fringe -*- lexical-binding: t; -*-
-;;
+;;; lean4-fringe.el --- Lean4-Mode Processing Progress in Fringe  -*- lexical-binding: t; -*-
+
 ;; Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-;; Released under Apache 2.0 license as described in the file LICENSE.
-;;
-;; Authors: Gabriel Ebner, Sebastian Ullrich
-;; SPDX-License-Identifier: Apache-2.0
 
-;;; License:
+;; This file is not part of GNU Emacs.
 
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
-;;
+
 ;; Show Lean processing progress in the editor fringe
-;;
+
 ;;; Code:
 
 (require 'lean4-settings)

diff --git a/lean4-info.el b/lean4-info.el
@@ -1,29 +1,21 @@
-;;; lean4-info.el --- Emacs mode for Lean theorem prover -*- lexical-binding: t -*-
+;;; lean4-info.el --- Lean4-Mode Info View  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2016 Gabriel Ebner. All rights reserved.
 ;; Copyright (c) 2024 Mekeor Melire
 
-;; Author: Gabriel Ebner <[email protected]>
-;; Maintainer: Gabriel Ebner <[email protected]>
-;; Created: Oct 29, 2016
-;; Keywords: languages
-;; Version: 0.1
-;; URL: https://github.com/leanprover/lean4-mode
-;; SPDX-License-Identifier: Apache-2.0
+;; This file is not part of GNU Emacs.
 
-;;; License:
-
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-input.el b/lean4-input.el
@@ -1,40 +1,29 @@
 ;;; lean4-input.el --- The Lean input method (based/copied from Agda) -*- lexical-binding: t -*-
-;;;
-;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language.
-;;; We did minor modifications
-;; SPDX-License-Identifier: Apache-2.0
-;;
-
-;;; License:
-
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
-;;
-;;     http://www.apache.org/licenses/LICENSE-2.0
-;;
-;; Unless required by applicable law or agreed to in writing, software
-;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+
+;; Copyright (c) 2005-2012 Ulf Norell, Nils Anders Danielsson,
+;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter,
+;; Marcin Benke, Darin Morrison.
 
 ;;; Commentary:
-;;
-;;;; A highly customisable input method which can inherit from other
+
+;; A highly customisable input method which can inherit from other
 ;; Quail input methods.  By default the input method is geared towards
 ;; the input of mathematical and other symbols in Lean programs.
-;;
+
 ;; Use M-x customize-group lean4-input to customise this input method.
 ;; Note that the functions defined under "Functions used to tweak
 ;; translation pairs" below can be used to tweak both the key
 ;; translations inherited from other input methods as well as the
 ;; ones added specifically for this one.
-;;
+
 ;; Use lean4-input-show-translations to see all the characters which
 ;; can be typed using this input method (except for those
 ;; corresponding to ASCII characters).
 
+;; This file is based on agda-input.el from Agda-Mode.  The Lean4
+;; community did minor modifications.
+;; https://github.com/agda/agda/blob/d2cbd2dd4f49fa84c5ca6fcf464c3211adcc0088/src/data/emacs-mode/agda-input.el
+
 ;;; Code:
 
 (require 'quail)
@@ -305,10 +294,7 @@ Suitable for use in the :set field of `defcustom'."
   (lean4-input-setup))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Administrative details
-
-(provide 'lean4-input)
-;;; lean4-input.el ends here
+;; Export Translations
 
 (defun lean4-input-export-translations ()
   "Export the current translations in a javascript format.
@@ -335,3 +321,9 @@ leanprover.github.io/tutorial/js/input-method.js"
   (lean4-input-export-translations)
   (with-current-buffer "*lean4-translations*"
     (princ (buffer-string))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Administrative details
+
+(provide 'lean4-input)
+;;; lean4-input.el ends here
diff --git a/lean4-lake.el b/lean4-lake.el
@@ -1,21 +1,18 @@
-;;; lean4-lake.el --- Lake integration for lean4-mode -*- lexical-binding: t -*-
+;;; lean4-lake.el --- Lean4-Mode Lake Integration  -*- lexical-binding: t; -*-
 
-;; SPDX-License-Identifier: Apache-2.0
 ;; This file is not part of GNU Emacs.
 
-;;; License:
-
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-mode.el b/lean4-mode.el
@@ -1,4 +1,4 @@
-;;; lean4-mode.el --- A major mode for the Lean language -*- lexical-binding: t -*-
+;;; lean4-mode.el --- Major Mode for Lean Language  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
 ;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved.
@@ -15,19 +15,19 @@
 ;; SPDX-License-Identifier: Apache-2.0
 ;; Version: 1.0.1
 
-;;; License:
+;; This file is not part of GNU Emacs.
 
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-settings.el b/lean4-settings.el
@@ -1,25 +1,20 @@
-;;; lean4-settings.el --- Custom variables for lean4-mode -*- lexical-binding: t -*-
+;;; lean4-settings.el --- Lean4-Mode User-Options  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-;; Released under Apache 2.0 license as described in the file LICENSE.
-;;
-;; Author: Soonho Kong
-;; SPDX-License-Identifier: Apache-2.0
-;;
 
-;;; License:
+;; This file is not part of GNU Emacs.
 
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary:
 

diff --git a/lean4-syntax.el b/lean4-syntax.el
@@ -1,25 +1,20 @@
-;;; lean4-syntax.el --- Syntax definitions for lean4-mode -*- lexical-binding: t -*-
+;;; lean4-syntax.el --- Lean4-Mode Syntax Definitions  -*- lexical-binding: t; -*-
 
 ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
-;; Released under Apache 2.0 license as described in the file LICENSE.
-;;
-;; Author: Leonardo de Moura
-;;         Soonho Kong
-;; SPDX-License-Identifier: Apache-2.0
 
-;;; License:
+;; This file is not part of GNU Emacs.
 
-;; Licensed under the Apache License, Version 2.0 (the "License");
-;; you may not use this file except in compliance with the License.
-;; You may obtain a copy of the License at:
+;; Licensed under the Apache License, Version 2.0 (the "License"); you
+;; may not use this file except in compliance with the License.  You
+;; may obtain a copy of the License at
 ;;
 ;;     http://www.apache.org/licenses/LICENSE-2.0
 ;;
 ;; Unless required by applicable law or agreed to in writing, software
 ;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-;; See the License for the specific language governing permissions and
-;; limitations under the License.
+;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+;; implied.  See the License for the specific language governing
+;; permissions and limitations under the License.
 
 ;;; Commentary: