radium-lang-ada.el

;;; radium-lang-ada.el, ada + spark via gnu elpa ada-mode + gnat/gnatprove -*- lexical-binding: t; -*-
;;
;; ada-mode was spun out of emacs core into a gnu elpa package (emacs
;; 26+), so it's pulled in via use-package/package.el like anything
;; else on melpa, not `require`d as a built-in.
 
(use-package ada-mode
  :mode (("\\.ads\\'" . ada-mode)
         ("\\.adb\\'" . ada-mode))
  :custom (ada-indent 8) ;; tabs, 8 wide, like everything else
  :hook (ada-mode . (lambda ()
                      (setq indent-tabs-mode t
                            tab-width 8))))
 
(defun radium-gnatprove ()
  "i run gnatprove (spark flow/proof analysis) against a .gpr in this dir."
  (interactive)
  (let ((gpr (or (car (directory-files default-directory nil "\\.gpr\\'"))
                 (read-string "project.gpr: "))))
    (compile (format "gnatprove -P%s" gpr))))
 
(with-eval-after-load 'ada-mode
  (define-key ada-mode-map (kbd "C-c C-p") #'radium-gnatprove))
 
(defun radium-ada-build-wisi-parser ()
  "i build + install ada-mode's own bundled ada parser (wisi/gpr, not an
lsp server) by running the build.sh/install.sh scripts it ships, inside
the actual installed package directory. one-time setup for full
semantic ada support; needs gprbuild + gnatprep on PATH."
  (interactive)
  (let* ((lib (locate-library "ada-mode"))
         (dir (and lib (file-name-directory lib))))
    (unless (and dir (file-exists-p (expand-file-name "build.sh" dir)))
      (user-error "err: cant find ada-mode's build.sh (looked in %s)." dir))
    (compile (format "cd %s && sh build.sh -j0 && sh install.sh"
                      (shell-quote-argument dir)))))
 
(global-set-key (kbd "C-c a w") #'radium-ada-build-wisi-parser)
 
(provide 'radium-lang-ada)