From ffe13bed631f9e295701fa1e63fe4cdbc2bef1ad Mon Sep 17 00:00:00 2001
From: Mekeor Melire <mekeor@posteo.de>
Date: Mon, 9 Dec 2024 00:16:06 +0100
Subject: [PATCH] Delete lean4-debug

Because it does not work.
---
 lean4-debug.el | 77 --------------------------------------------------
 1 file changed, 77 deletions(-)
 delete mode 100644 lean4-debug.el

diff --git a/lean4-debug.el b/lean4-debug.el
deleted file mode 100644
index 5d86a1c..0000000
--- a/lean4-debug.el
+++ /dev/null
@@ -1,77 +0,0 @@
-;;; lean4-debug.el --- Lean4-Mode Debug Mode  -*- lexical-binding: t; -*-
-
-;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-
-;; 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
-;;
-;;     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.
-
-;;; Commentary:
-
-;; This library provides a debug mode for `lean4-mode'.
-
-;;; Code:
-
-(require 'cl-lib)
-
-(defvar lean4-debug-mode nil)
-
-(defvar lean4-debug-buffer-name "*lean4-debug*")
-
-(defun lean4-turn-on-debug-mode (&optional print-msg)
-  "Turn on Lean debug.
-Print message \"lean: turn on debug mode\" if PRINT-MSG or if called
-interactively."
-  (interactive)
-  (when (or (called-interactively-p 'any) print-msg)
-    (message "lean: turn on debug mode"))
-  (get-buffer-create lean4-debug-buffer-name)
-  (buffer-disable-undo lean4-debug-buffer-name)
-  (display-buffer lean4-debug-buffer-name 'display-buffer-reuse-window
-                  '((reusable-frames . t)))
-  (setq lean4-debug-mode t))
-
-(defun lean4-turn-off-debug-mode (&optional print-msg)
-  "Turn off Lean debug.
-Print message \"lean: turn off debug mode\" if PRINT-MSG or if called
-interactively."
-  (interactive)
-  (when (derived-mode-p 'lean4-mode)
-    (when (or (called-interactively-p 'any) print-msg)
-      (message "lean: turn off debug mode"))
-    (setq lean4-debug-mode nil)))
-
-(defun lean4-output-to-buffer (buffer-name format-string args)
-  "Output a message to a buffer.
-The buffer is given by BUFFER-NAME.  The message is given by FORMAT-STRING
-and ARGS."
-  (with-current-buffer
-      (get-buffer-create buffer-name)
-    (save-selected-window
-      (ignore-errors
-        (select-window (get-buffer-window buffer-name t)))
-      (goto-char (point-max))
-      (insert (apply #'format format-string args)))))
-
-(defun lean4-debug (format-string &rest args)
-  "Display a message at the bottom of the *lean4-debug* buffer.
-The message is given by FORMAT-STRING and ARGS."
-  (when lean4-debug-mode
-    (let ((time-str (format-time-string "%T.%3N" (current-time))))
-      (lean4-output-to-buffer lean4-debug-buffer-name
-                             (concat "%s -- " format-string "\n")
-                             (cons (propertize time-str 'face 'font-lock-keyword-face)
-                                   args)))))
-
-(provide 'lean4-debug)
-;;; lean4-debug.el ends here