Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
215 lines (184 sloc) 7.37 KB
(eval-when-compile
(require 'comint))
(defvar ivor-mode-map
(let ((map (make-sparse-keymap)))
(define-key map "\C-j" 'newline-and-indent)
(define-key map "\C-n" 'ivor-send-to-shell)
(define-key map "\C-c\C-n" 'ivor-send-all-to-shell)
(define-key map "\C-c\C-s" 'ivor-start)
(define-key map "\C-c\C-d" 'ivor-stop)
(define-key map "\C-c\C-r" 'ivor-restart)
(define-key map "\C-c\C-u" 'ivor-undo)
map)
"Keymap for `ivor-mode'.")
(add-to-list 'auto-mode-alist '("\\.tt\\'" . ivor-mode))
(defvar ivor-mode-syntax-table
(let ((st (make-syntax-table)))
(modify-syntax-entry ?{ ". 1" st)
(modify-syntax-entry ?} ". 4" st)
(modify-syntax-entry ?- ". 1b2b3" st)
(modify-syntax-entry ?\n "> b" st)
st)
"Syntax table for `ivor-mode'.")
;;;(regexp-opt '("Data" "Rec" "Qed" "Freeze" "Thaw" "Eval" "Check" "Load"
;;; "Suspend" "Resume" "Compile" "Repl" "Equality" "Drop"
;;; "Primitives" "Forget" "Let" "Axiom" "Focus" "Declare" "Where"
;;; "Plugin"))
;;;(regexp-opt '("attack" "claim" "local" "refine" "solve" "fill" "return"
;;; "quote" "call" "abandon" "rename" "intro" "intros" "arg"
;;; "equiv" "generalise" "dependent" "replace" "axiomatise"
;;; "compute" "unfold" "trivial" "by" "induction" "case"
;;; "auto" "left" "right" "split" "exists" "decide"))
(defconst ivor-font-lock-keywords
(list '("\\<\\(Axiom\\|C\\(?:heck\\|ompile\\)\\|D\\(?:ata\\|eclare\\|rop\\)\\|E\\(?:quality\\|val\\)\\|F\\(?:o\\(?:cus\\|rget\\)\\|reeze\\)\\|L\\(?:et\\|oad\\)\\|Primitives\\|Qed\\|Re\\(?:c\\|pl\\|sume\\)\\|Suspend\\|Thaw\\|Plugin\\|Where\\)\\>"
. font-lock-keyword-face)
'("a\\(?:bandon\\|rg\\|ttack\\|uto\\|xiomatise\\)\\|by\\|c\\(?:a\\(?:ll\\|se\\)\\|laim\\|ompute\\)\\|de\\(?:cide\\|pendent\\)\\|e\\(?:quiv\\|xists\\)\\|fill\\|generalise\\|in\\(?:duction\\|tros?\\)\\|l\\(?:eft\\|ocal\\)\\|quote\\|r\\(?:e\\(?:fine\\|name\\|place\\|turn\\)\\|ight\\)\\|s\\(?:olve\\|plit\\)\\|trivial\\|unfold" . font-lock-builtin-face)
'("<\\([^:]*\\):[^>]*>" . (1 font-lock-string-face keep t))
'("<\\([^>:]*\\)>" . (1 font-lock-string-face keep t))
'("^\\([a-zA-Z0-9\\'\\_]+\\)\\s-*:" . (1 font-lock-function-name-face keep t))
'("^\\([a-zA-Z0-9\\'\\_]+\\)\\s-*=" . (1 font-lock-function-name-face keep t))
'("Rec\\s-+\\([a-zA-Z0-9\\'\\_]+\\)\\s-*:" . (1 font-lock-function-name-face t t))
'("\\b\\([a-zA-Z0-9\\'\\_]+\\)\\s-*:" . (1 font-lock-variable-name-face keep t))
'("\\b\\([a-zA-Z0-9\\'\\_]+\\)\\s-*," . (1 font-lock-variable-name-face keep t))
)
"Highlighting for Ivor mode")
;;;(defvar tt-font-lock-keywords
;;; '(("Data" (1 font-lock-keyword-face)))
;;; "Keyword highlighting specification for `ivor-mode'.")
;;(defvar tt-imenu-generic-expression
;; ...)
;;(defvar tt-outline-regexp
;; ...)
;;;###autoload
(define-derived-mode ivor-mode fundamental-mode "Ivor"
"A major mode for editing Ivor files."
(set (make-local-variable 'comment-start) "-- ")
(set (make-local-variable 'comment-start-skip) "#+\\s-*")
(set (make-local-variable 'font-lock-defaults)
'(ivor-font-lock-keywords))
(set (make-local-variable 'indent-line-function) 'ivor-indent-line)
;; (set (make-local-variable 'imenu-generic-expression)
;; ivor-imenu-generic-expression)
;; (set (make-local-variable 'outline-regexp) ivor-outline-regexp)
)
;;; Indentation
;; 1. Qed line is indented to 0
;; 2. After 'Data' indent each line 4 until a semicolon, or 2 if the line
;; begins with '|' or '='
(defun ivor-indent-line ()
"Indent current line of Ivor code."
(interactive)
(let ((savep (> (current-column) (current-indentation)))
(indent (condition-case nil (max (ivor-calculate-indentation) 0)
(error 0))))
(if savep
(save-excursion (indent-line-to indent))
(indent-line-to indent))))
(defun ivor-calculate-indentation ()
"Return the column to which the current line should be indented."
;; Default is the indentation of the previous line
(cond
((ivor-isQed) 0)
((ivor-first-is "[ \\t]*|") (ivor-under-eq))
((ivor-eq-no-semi) 4)
((ivor-first-is "[ \\t]*=") 2)
(t (ivor-get-previous-indentation))
)
)
(defun ivor-isQed ()
(save-excursion
(beginning-of-line)
(looking-at "Qed")))
(defun ivor-eq-no-semi ()
(save-excursion
(forward-line -1)
(beginning-of-line)
(looking-at ".*=[^;]*$")))
(defun ivor-under-eq ()
"Indent to under the = sign on the previous line, or 4 spaces if none"
(save-excursion
(forward-line -1)
(beginning-of-line)
(let ((this-line (thing-at-point 'line)))
(let ((eq-point (string-match "=" this-line)))
(progn (if (eq eq-point nil)
2
eq-point))))))
(defun ivor-first-is (str)
(save-excursion
(beginning-of-line)
(looking-at str)))
(defun ivor-get-previous-indentation ()
"Return the indentation of the previous line"
(save-excursion
(forward-line -1)
(current-indentation)))
(defun ivor-send-to-shell ()
"Read the current line and send it to the shell process, if any"
(interactive)
(progn (save-excursion
(beginning-of-line)
(let* ((this-line (thing-at-point 'line))
(chomped (substring this-line 0 (- (length this-line) 1))))
(progn (set-buffer (get-buffer "*Ivor*"))
(insert chomped)
(comint-send-input))))
(forward-line 1)
(beginning-of-line)
)
)
(defun ivor-send-all-to-shell ()
"Send the buffer up to the current point to the shell process"
(interactive)
(let ((contents (buffer-substring 1 (point))))
(progn (set-buffer (get-buffer "*Ivor*"))
(insert contents)
(comint-send-input))))
(defvar ivor-shell-exec "jones")
(defvar ivor-shell-sep ";")
(defun set-ivor-shell (executable)
"Set the Ivor shell executable"
(interactive "sShell executable: ")
(setq ivor-shell-exec executable))
(defun set-ivor-sep (sep)
"Set the Ivor shell command separator"
(interactive "sShell separator: ")
(setq ivor-shell-sep sep))
(defun ivor-start ()
"Start a shell with Ivor in it"
(interactive)
(when (not (bufferp (get-buffer "*Ivor*")))
(progn (shell "*Ivor*")
(set-buffer (get-buffer "*Ivor*"))
(insert ivor-shell-exec)
(comint-send-input))))
(defun ivor-stop ()
"Stop the Ivor process"
(interactive)
(let ((dir (file-name-directory buffer-file-name)))
(save-current-buffer
(progn (set-buffer (get-buffer "*Ivor*"))
(insert (concat "Drop" ivor-shell-sep))
(comint-send-input))))
(goto-char (point-min)))
(defun ivor-restart ()
"Restart the Ivor process"
(interactive)
(let ((dir (file-name-directory buffer-file-name)))
(save-current-buffer
(progn (set-buffer (get-buffer "*Ivor*"))
(insert (concat "Drop" ivor-shell-sep))
(comint-send-input)
(insert (concat "cd " dir "; " ivor-shell-exec))
(comint-send-input))))
(goto-char (point-min)))
(defun ivor-undo-proof ()
"Send undo command in a proof state."
(interactive)
(let ((dir (file-name-directory buffer-file-name)))
(save-current-buffer
(progn (set-buffer (get-buffer "*Ivor*"))
(insert "Undo;")
(comint-send-input))))
(goto-char (point-min)))
(provide 'ivor-mode)