From c30b67632d65a3d69cac8ce15bf2d6db784b8bf8 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Wed, 27 Nov 2024 02:23:11 +0100 Subject: [PATCH] Rework headers; add missing copyright notice --- lean4-debug.el | 19 +++++++------------ lean4-dev.el | 19 +++++++------------ lean4-eri.el | 23 +++++++++++++---------- lean4-fringe.el | 26 +++++++++++--------------- lean4-info.el | 24 ++++++++---------------- lean4-input.el | 46 +++++++++++++++++++--------------------------- lean4-lake.el | 17 +++++++---------- lean4-mode.el | 16 ++++++++-------- lean4-settings.el | 21 ++++++++------------- lean4-syntax.el | 21 ++++++++------------- lean4-util.el | 20 ++++++++------------ 11 files changed, 104 insertions(+), 148 deletions(-) diff --git a/lean4-debug.el b/lean4-debug.el index ac5342f..162807c 100644 --- 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 index a1b9619..f9cc5ba 100644 --- 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 index 85be9fa..1ff9fcc 100644 --- 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 index b81ae8c..77490eb 100644 --- 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 index 9ee3cd8..c93c4e8 100644 --- 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 -;; Maintainer: Gabriel Ebner -;; 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 index 2698505..bc1fd10 100644 --- 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 index 37d32df..bfca627 100644 --- 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 index 9e6c2bb..24e7977 100644 --- 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 index 53cd9ed..dc5c246 100644 --- 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 index 4963565..e9a141d 100644 --- 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: diff --git a/lean4-util.el b/lean4-util.el index 4af725e..6cf64d0 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -1,24 +1,20 @@ -;;; lean4-util.el --- Utilities for lean4-mode -*- lexical-binding: t -*- +;;; lean4-util.el --- Lean4-Mode Utilities -*- 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: