<commit_before> ;;; red-jonprl-mode.el --- Red-Jonprl-Mode major mode

(defvar red-jonprl-map
  (let ((map (make-sparse-keymap)))
    map)
  "Keymap for `red-jonprl-mode'.")

(defvar red-jonprl-syntax-table
  (let ((st (make-syntax-table)))
    st)
  "Syntax table for `red-jonprl-mode'.")

(defvar red-jonprl-vernacular-keywords-regexp
  (regexp-opt
   '("Def" "Thm" "Tac")
   'words))

(defvar red-jonprl-builtin-constants-regexp
  (regexp-opt
   '("Base" "lbase" "lsuc" "Ax" "Univ" "member" "Squash" "Species" "extract")
   'words))

(defvar red-jonprl-sorts-regexp
  (regexp-opt
   '("exp" "lvl" "tac" "thm")
   'words))

(defvar red-jonprl-tactic-name-regexp
  (regexp-opt
   '("auto" "eval-goal" "ceval" "csym" "cstep" "witness" "trace")
   'words))

(defun red-jonprl-font-lock-defaults ()
  `((,red-jonprl-vernacular-keywords-regexp . font-lock-keyword-face)
    ("^\\s-*\\(//.*\\)$" . font-lock-comment-face)
    (,red-jonprl-builtin-constants-regexp . font-lock-constant-face)
    (,red-jonprl-sorts-regexp . font-lock-type-face)
    (,red-jonprl-tactic-name-regexp . font-lock-function-name-face)))

(define-derived-mode red-jonprl-mode fundamental-mode "red-jonprl"
  :syntax-table red-jonprl-syntax-table
  (setq-local comment-start "// ")
  (setq-local comment-start-skip "//+\\s-*")
  (setq-local indent-tabs-mode nil)
  (setq-local tab-width 2)
  (setq-local font-lock-defaults '((red-jonprl-font-lock-defaults)))
  (setq-local imenu-generic-expression
              '(("Theorems" "^Thm\\s-+\\(\\w+\\)" 1)
                ("Definitions" "^Def\\s-+\\(\\w+\\)" 1)
                ("Tactics" "^Tac\\s-+\\(\\w+\\)" 1)))
  )


(provide 'red-jonprl-mode)
(push '("\\.prl\\'" . red-jonprl-mode) auto-mode-alist)
 ;;; red-jonprl-mode.el ends here<commit_msg>[emacs] further cleanup<commit_after> ;;; red-jonprl-mode.el --- Red-Jonprl major mode

(defvar red-jonprl-map
  (let ((map (make-sparse-keymap)))
    map)
  "Keymap for `red-jonprl-mode'.")

(defvar red-jonprl-syntax-table
  (let ((st (make-syntax-table)))
    st)
  "Syntax table for `red-jonprl-mode'.")

(defvar red-jonprl-vernacular-keywords-regexp
  (regexp-opt
   '("Def" "Thm" "Tac")
   'words))

(defvar red-jonprl-builtin-constants-regexp
  (regexp-opt
   '("Base" "lbase" "lsuc" "Ax" "Univ" "member" "Squash" "Species" "extract")
   'words))

(defvar red-jonprl-sorts-regexp
  (regexp-opt
   '("exp" "lvl" "tac" "thm")
   'words))

(defvar red-jonprl-tactic-name-regexp
  (regexp-opt
   '("auto" "eval-goal" "ceval" "csym" "cstep" "witness" "trace")
   'words))

(defun red-jonprl-font-lock-defaults ()
  `((,red-jonprl-vernacular-keywords-regexp . font-lock-keyword-face)
    ("^\\s-*\\(//.*\\)$" . font-lock-comment-face)
    (,red-jonprl-builtin-constants-regexp . font-lock-constant-face)
    (,red-jonprl-sorts-regexp . font-lock-type-face)
    (,red-jonprl-tactic-name-regexp . font-lock-function-name-face)))

(defun red-jonprl-imenu-generic-expression ()
  "To generate a table of contents for a Red JonPRL signature"
  '(("Definitions" "^Def\\s-+\\(\\w+\\)" 1)
    ("Theorems" "^Thm\\s-+\\(\\w+\\)" 1)
    ("Tactics" "^Tac\\s-+\\(\\w+\\)" 1)))

(define-derived-mode red-jonprl-mode fundamental-mode "red-jonprl"
  :syntax-table red-jonprl-syntax-table
  (setq-local comment-start "// ")
  (setq-local comment-start-skip "//+\\s-*")
  (setq-local indent-tabs-mode nil)
  (setq-local tab-width 2)
  (setq-local font-lock-defaults '((red-jonprl-font-lock-defaults)))
  (setq-local imenu-generic-expression (red-jonprl-imenu-generic-expression)))

(push '("\\.prl\\'" . red-jonprl-mode) auto-mode-alist)

(provide 'red-jonprl-mode)
 ;;; red-jonprl-mode.el ends here
{'fraction_non_alphanumeric': 0.21908417877707706, 'fraction_numerical': 0.0021935837674801205, 'mean_word_length': 3.217341040462428, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3273566', 'n_tokens_mistral': 1586, 'n_tokens_neox': 1538, 'n_words': 245}