2025-09-07 18:02:30 -07:00
|
|
|
;;; perga-mode.el --- major mode for perga -*- lexical-binding: t; -*-
|
|
|
|
|
|
|
|
|
|
;; Author: William Ball <wball@ballcloud.cc>
|
|
|
|
|
;; Maintainer: William Ball <wball@ballcloud.cc>
|
|
|
|
|
;; Version: 0.1
|
|
|
|
|
;; Package-Requires: ((emacs "29.1"))
|
|
|
|
|
;; Homepage: https://forgejo.ballcloud.cc/wball/perga-mode
|
|
|
|
|
;; Keywords: languages, tree-sitter
|
|
|
|
|
|
|
|
|
|
;; This file is not part of GNU Emacs.
|
|
|
|
|
|
|
|
|
|
;;; Commentary:
|
|
|
|
|
|
|
|
|
|
;; Major mode for editing perga code, with Tree-sitter-based
|
|
|
|
|
;; font-lock support. Requires Emacs 29 or newer.
|
|
|
|
|
|
|
|
|
|
;;; Code:
|
|
|
|
|
|
|
|
|
|
(require 'treesit)
|
|
|
|
|
|
|
|
|
|
(defun perga--ensure-treesit-grammar ()
|
|
|
|
|
"Ensure the perga Tree-sitter grammar is installed."
|
|
|
|
|
(unless (treesit-ready-p 'perga)
|
|
|
|
|
(add-to-list 'treesit-language-source-alist
|
2025-11-21 16:05:03 -08:00
|
|
|
'(perga . ("https://forgejo.ballcloud.cc/wball/tree-sitter-perga")))
|
2025-09-07 18:02:30 -07:00
|
|
|
(when (yes-or-no-p "Tree-sitter grammar for perga not found. Install it now? ")
|
|
|
|
|
(treesit-install-language-grammar 'perga))))
|
|
|
|
|
|
|
|
|
|
(defvar perga--font-lock-rules
|
|
|
|
|
'(:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature keyword
|
|
|
|
|
([ "fun" "λ" "forall" "∏" "let" "in" "end" "def" "axiom" "variable" "hypothesis" "section" "infixl" "infixr" "[" "]" ] @font-lock-keyword-face)
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature preprocessor
|
|
|
|
|
((preprocess
|
|
|
|
|
(command) @font-lock-preprocessor-face
|
|
|
|
|
(post_command) @font-lock-string-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature delimiter
|
|
|
|
|
([ "=>" "→" "⇒" "," ":=" ";" ":" ] @font-lock-delimiter-face)
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature operator
|
|
|
|
|
((symbol) @font-lock-operator-face)
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature constant
|
|
|
|
|
([(star) (square)] @font-lock-constant-face)
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature comment
|
|
|
|
|
((comment) @font-lock-comment-face)
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature definition
|
|
|
|
|
((definition
|
|
|
|
|
name: (identifier) @font-lock-function-name-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature definition
|
|
|
|
|
((axiom
|
|
|
|
|
name: (identifier) @font-lock-function-name-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature assignment
|
|
|
|
|
((binding
|
|
|
|
|
(identifier) @font-lock-function-name-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature parameter
|
|
|
|
|
((param_block
|
|
|
|
|
param: (identifier)+ @font-lock-variable-name-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature type
|
|
|
|
|
((param_block
|
|
|
|
|
type: (expr) @font-lock-type-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature type
|
|
|
|
|
((labs_alt
|
|
|
|
|
type: (expr) @font-lock-type-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature parameter
|
|
|
|
|
((labs_alt
|
|
|
|
|
param: (identifier)+ @font-lock-variable-name-face))
|
|
|
|
|
|
|
|
|
|
:language perga
|
|
|
|
|
:override t
|
|
|
|
|
:feature type
|
|
|
|
|
((ascription
|
|
|
|
|
type: (expr) @font-lock-type-face))))
|
|
|
|
|
|
|
|
|
|
(defun perga--setup ()
|
|
|
|
|
"Setup treesit for perga-mode."
|
|
|
|
|
(setq-local treesit-font-lock-settings
|
|
|
|
|
(apply #'treesit-font-lock-rules
|
|
|
|
|
perga--font-lock-rules))
|
|
|
|
|
|
|
|
|
|
(setq-local font-lock-defaults nil)
|
|
|
|
|
|
|
|
|
|
(setq-local treesit-font-lock-feature-list
|
|
|
|
|
'((comment definition)
|
|
|
|
|
(keyword type constant preprocessor)
|
|
|
|
|
(assignment parameter delimiter operator)))
|
|
|
|
|
|
|
|
|
|
(setq-local treesit-font-lock-level 3)
|
|
|
|
|
|
|
|
|
|
;; (setq-local treesit-simple-indent-rules
|
|
|
|
|
;; `((perga
|
|
|
|
|
;; ((parent-is "program") column-0 0)
|
|
|
|
|
;; ((node-is ":=") parent 4)
|
|
|
|
|
;; ((parent-is "definition") parent 4)
|
|
|
|
|
;; ((parent-is "labs") parent 4)
|
|
|
|
|
;; (no-node parent 0))))
|
|
|
|
|
|
|
|
|
|
(treesit-major-mode-setup))
|
|
|
|
|
|
|
|
|
|
;;;###autoload
|
|
|
|
|
(define-derived-mode perga-mode prog-mode "perga"
|
|
|
|
|
"Major mode for perga files."
|
|
|
|
|
(perga--ensure-treesit-grammar)
|
|
|
|
|
(when (treesit-ready-p 'perga)
|
|
|
|
|
(treesit-parser-create 'perga)
|
|
|
|
|
(perga--setup)))
|
|
|
|
|
|
|
|
|
|
(defun perga-typecheck-current-file ()
|
|
|
|
|
"Typecheck the current file using the `perga` executable"
|
|
|
|
|
(interactive))
|
|
|
|
|
|
|
|
|
|
(defvar perga-mode-map
|
|
|
|
|
(let ((map (make-sparse-keymap)))
|
|
|
|
|
(define-key map "C-c c" #'do-stuff)
|
|
|
|
|
map))
|
|
|
|
|
|
|
|
|
|
(provide 'perga-mode)
|
|
|
|
|
|
|
|
|
|
;;;###autoload
|
|
|
|
|
(add-to-list 'auto-mode-alist '("\\.pg" . perga-mode))
|
|
|
|
|
|
|
|
|
|
;;; perga-mode.el ends here
|