From 50abe8352b047deb9ba4f1cfd0720de883c84909 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 1 Nov 2020 18:16:44 +0100
Subject: [PATCH] feat: allow specifying file name with --stdin

---
 lean4-mode/lean4-flycheck.el | 8 +-------
 src/shell/lean.cpp           | 7 +++----
 stage0/src/shell/lean.cpp    | 7 +++----
 3 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/lean4-mode/lean4-flycheck.el b/lean4-mode/lean4-flycheck.el
index f558de1e1b..e3041bef58 100644
--- a/lean4-mode/lean4-flycheck.el
+++ b/lean4-mode/lean4-flycheck.el
@@ -23,7 +23,7 @@
          (-concat `(,(lean4-get-executable lean4-executable-name))
                   '((eval lean4-extra-arguments))
                   extra-args
-                  '("--json" "--stdin"))))
+                  '("--json" "--stdin" source-original))))
     command))
 
 (cl-defun lean4-flycheck-parse-task (checker buffer cur-file-name
@@ -106,12 +106,6 @@
     :standard-input t
     :error-parser #'lean4-flycheck-parse-errors
     :modes '(lean4-mode))
-  (flycheck-define-command-checker 'lean4-bootstrapped-checker
-    "Bootstrapped Lean syntax checker."
-    :command (lean4-flycheck-command '("--new-frontend"))
-    :standard-input t
-    :error-parser #'lean4-flycheck-parse-errors
-    :modes '(lean4-mode))
   (add-to-list 'flycheck-checkers 'lean4-checker))
 
 (defun lean4-flycheck-turn-on ()
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 358e1f6ade..b92a1f8ceb 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -590,11 +590,10 @@ int main(int argc, char ** argv) {
     try {
         if (use_stdin) {
             if (argc - optind != 0) {
-                std::cerr << "Expected exactly one of file name or --stdin\n";
-                display_help(std::cerr);
-                return 1;
+                mod_fn = argv[optind++];
+            } else {
+                mod_fn = "<stdin>";
             }
-            mod_fn = "<stdin>";
             std::stringstream buf;
             buf << std::cin.rdbuf();
             contents = buf.str();
diff --git a/stage0/src/shell/lean.cpp b/stage0/src/shell/lean.cpp
index 358e1f6ade..b92a1f8ceb 100644
--- a/stage0/src/shell/lean.cpp
+++ b/stage0/src/shell/lean.cpp
@@ -590,11 +590,10 @@ int main(int argc, char ** argv) {
     try {
         if (use_stdin) {
             if (argc - optind != 0) {
-                std::cerr << "Expected exactly one of file name or --stdin\n";
-                display_help(std::cerr);
-                return 1;
+                mod_fn = argv[optind++];
+            } else {
+                mod_fn = "<stdin>";
             }
-            mod_fn = "<stdin>";
             std::stringstream buf;
             buf << std::cin.rdbuf();
             contents = buf.str();