dynamic highlighting

[ElifUskuplu]

I am very beginner in PG, and trying to adapt it to an experimental proof assistant. Initially, I created a simple emacs mode file with a dynamic highlighting property:

(defvar PA-dynamic-terms '()
  "List of dynamically identified terms for highlighting.")

(defun PA-update-dynamic-terms ()
  "Parse the buffer for user-defined constants following 'axiom|def const'  and update dynamic terms."
  (save-excursion
    (goto-char (point-min))
    (let ((terms '()))
      (setq PA-dynamic-terms '())
      (while (re-search-forward "\\(axiom\\|def\\) \\(\\w+\\(?:_\\w+\\)*\\)\\(?:\\s-+\\(?:\\(.*?\\)\\s-*:\\)?\\)\\s-*" nil t)
        (let ((const-name (match-string 2)))
          (unless (member const-name terms)
            (push const-name terms))))
      ;; Remove duplicates and update the global list
      (setq PA-dynamic-terms (delete-dups terms)))))

(defun PA-apply-dynamic-highlighting ()
  "Apply dynamic highlighting for terms in `PA-dynamic-terms`."
  (font-lock-add-keywords nil `((,(regexp-opt PA-dynamic-terms 'words) . 'font-lock-function-name-face)) t))

(define-derived-mode pa fundamental-mode "PA"
  "A mode for editing my language files."
  ;; Apply dynamic highlighting after changes
  (add-hook 'after-change-functions (lambda (start end old-len)
                                      (PA-update-dynamic-terms)
                                      (PA-apply-dynamic-highlighting))
            nil t)
  ;; Initialize dynamic highlighting
  (PA-update-dynamic-terms)
  (PA-apply-dynamic-highlighting))

(provide 'pa)

How can I do the same using Proof General? Or is there any feature of PG that allowing such highlighting rules?

[ElifUskuplu]

Actually, I solved my problem. After providing PA-apply-dynamic-highlighting, I also defined

(defun PA-refresh-font-lock ()
  "Refresh font lock to apply dynamic highlighting."
  (font-lock-flush)
  (font-lock-ensure))

(defun PA-after-change-function (start end len)
  "Function to be called after changes to update and apply dynamic highlighting."
  (PA-update-dynamic-terms)
  (PA-apply-dynamic-highlighting)
  (PA-refresh-font-lock))

Then, I added it to hook:

add-hook 'PA-mode-hook
          (lambda ()
            (add-hook 'after-change-functions 'PA-after-change-function nil t)))

I wonder is there any easier way, or any proof-easy-config variable that I can use?