Extract proper filename for flycheck on related locations in refining modules

[xinhaoyuan]

Example - http://rise4fun.com/Dafny/Ute6

When a error is related to parent module of a refinement, Dafny will output error lines as "X.dfy[Y]: ...", and current error pattern will interpret the filename as "X.dfy[Y]".

Here is my local fix in .emacs, it also contains a workaround attempt of https://github.com/boogie-org/boogie-friends/issues/8.

(setq old-parse-errors (symbol-function 'inferior-dafny-parse-errors))
;; a workaround for removing [module-name] and dealing with external file locations
(defun inferior-dafny-parse-errors (errors)
(mapc (lambda (e)
        (let ((fname (flycheck-error-filename e)))
          (if (eq fname nil)
              (setq fname buffer-file-name)
            (if (string-match
                 (rx (group (* (not (in "[]")))) (* anything))
                 fname)
                (setq fname (match-string 1 fname)))
            (if (not (string-equal fname buffer-file-name))
                (let ((old-fname (flycheck-error-filename e))
                      (old-msg (flycheck-error-message e))
                      (old-col (flycheck-error-column e))
                      (old-line (flycheck-error-line e)))
                  (setf (flycheck-error-message e)
                        (concat (format "%s(%d:%d)-"
                                        (file-name-nondirectory fname)
                                        old-line
                                        old-col
                                        )
                                old-msg
                                "(" old-fname ")"))
                  (setf (flycheck-error-column e) nil)
                  ;; since line is required ...
                  (setf (flycheck-error-line e) 1)
                  (setq fname buffer-file-name))))
          (setf (flycheck-error-filename e) fname)
          ))
      (funcall old-parse-errors errors)))