max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: allow specifying file name with --stdin

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-01 18:16:44 +01:00
parent 8b027235dc
commit 50abe8352b
3 changed files with 7 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lean4-mode/lean4-flycheck.el
View file

@ -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 ()

7
src/shell/lean.cpp
View file

@ -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();

7
stage0/src/shell/lean.cpp generated
View file

@ -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();