michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-flycheck): support windows

Browse source 
In windows, we need to first call python interpreter to call linja.
This commit is contained in:
Soonho Kong 2014-09-19 09:37:56 -07:00
parent 8fe7465ade
commit af4e18dd44
1 changed files with 26 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/emacs/lean-flycheck.el
View file

@ -9,14 +9,18 @@
(defun lean-flycheck-command () (defun lean-flycheck-command ()
"Concat lean-flychecker-checker-name with options" "Concat lean-flychecker-checker-name with options"
(cl-concatenate 'list (let ((command
`(,(lean-get-executable lean-flycheck-checker-name)) (cl-concatenate 'list
lean-flycheck-checker-options `(,(lean-get-executable lean-flycheck-checker-name))
'("--cache") lean-flycheck-checker-options
'(source-original) '("--cache")
'((eval (lean-option-string))) '(source-original)
'("--") '((eval (lean-option-string)))
'(source-inplace))) '("--")
'(source-inplace))))
(when (string= system-type "windows-nt")
(setq command (cons "python" command)))
command))
(defun lean-flycheck-init () (defun lean-flycheck-init ()
"Initialize lean-flychek checker" "Initialize lean-flychek checker"
@ -25,15 +29,25 @@
"A Lean syntax checker." "A Lean syntax checker."
:command ,(lean-flycheck-command) :command ,(lean-flycheck-command)
:error-patterns :error-patterns
((error line-start "FLYCHECK_BEGIN ERROR\n" ;; ((error line-start "FLYCHECK_BEGIN ERROR" (? "\r") "\n"
;; (file-name) ":" line ":" (? column ":") " error: "
;; (minimal-match
;; (message (+ (+ not-newline) (? "\r") "\n")))
;; "FLYCHECK_END" line-end)
;; (warning line-start "FLYCHECK_BEGIN WARNING" (? "\r") "\n"
;; (file-name) ":" line ":" (? column ":") " warning "
;; (minimal-match
;; (message (+ (* not-newline) (? "\r") "\n") ))
;; "FLYCHECK_END" line-end))
((error line-start "FLYCHECK_BEGIN ERROR" (? "\r") "\n"
(file-name) ":" line ":" (? column ":") " error: " (file-name) ":" line ":" (? column ":") " error: "
(minimal-match (minimal-match
(message (one-or-more (one-or-more not-newline) "\n") )) (message (one-or-more (one-or-more not-newline) (? "\r") "\n")))
"FLYCHECK_END" line-end) "FLYCHECK_END" line-end)
(warning line-start "FLYCHECK_BEGIN WARNING\n" (warning line-start "FLYCHECK_BEGIN WARNING" (? "\r") "\n"
(file-name) ":" line ":" (? column ":") " warning " (file-name) ":" line ":" (? column ":") " warning "
(minimal-match (minimal-match
(message (one-or-more (one-or-more not-newline) "\n") )) (message (one-or-more (one-or-more not-newline) (? "\r") "\n")))
"FLYCHECK_END" line-end)) "FLYCHECK_END" line-end))
:modes (lean-mode))) :modes (lean-mode)))
(add-to-list 'flycheck-checkers 'lean-checker)) (add-to-list 'flycheck-checkers 'lean-checker))