mirror of
https://github.com/anoma/juvix.git
synced 2024-12-12 04:43:18 +03:00
Move juvix-mode to a separate repository (#1744)
The new repo is https://github.com/anoma/juvix/mode
This commit is contained in:
parent
43d114f9b1
commit
9de850df75
@ -3,11 +3,17 @@
|
||||
There is an Emacs mode available for Juvix. Currently, it
|
||||
supports syntax highlighting for well-scoped modules.
|
||||
|
||||
To get started, clone the Juvix Emacs mode repository:
|
||||
|
||||
#+begin_src sh
|
||||
git clone https://github.com/anoma/juvix-mode.git
|
||||
#+end_src
|
||||
|
||||
To install it add the following lines to your
|
||||
Emacs configuration file:
|
||||
|
||||
#+begin_src elisp
|
||||
(push "/path/to/juvix/juvix-mode/" load-path)
|
||||
(push "/path/to/juvix-mode/" load-path)
|
||||
(require 'juvix-mode)
|
||||
#+end_src
|
||||
|
||||
|
@ -1,29 +0,0 @@
|
||||
(require 'flycheck)
|
||||
(require 'juvix-customize)
|
||||
|
||||
(defgroup flycheck-juvix nil
|
||||
"Juvix support for Flycheck."
|
||||
:prefix "flycheck-juvix-"
|
||||
:group 'flycheck
|
||||
:link '(url-link :tag "Github" "https://github.com/anoma/juvix"))
|
||||
|
||||
(flycheck-define-checker juvix
|
||||
"A Juvix syntax checker."
|
||||
:command ("juvix" "--only-errors" "--no-colors" "--stdin"
|
||||
(option-flag "--no-stdlib" juvix-disable-embedded-stdlib)
|
||||
(option "--stdlib-path" juvix-stdlib-path)
|
||||
"typecheck"
|
||||
source-original)
|
||||
:standard-input t
|
||||
:error-patterns
|
||||
(
|
||||
(error line-start (file-name) ":" line ":" column ": error:" (message (one-or-more (not "ת"))))
|
||||
(error line-start (file-name) ":" line ":" column "-" end-column ": error:" (message (one-or-more (not "ת"))))
|
||||
(error line-start (file-name) ":" line "-" end-line ":" column ": error:" (message (one-or-more (not "ת"))))
|
||||
(error line-start (file-name) ":" line "-" end-line ":" column "-" end-column ": error:" (message (one-or-more (not "ת"))))
|
||||
)
|
||||
:modes juvix-mode
|
||||
)
|
||||
(add-to-list 'flycheck-checkers 'juvix)
|
||||
|
||||
(provide 'flycheck-juvix)
|
@ -1,17 +0,0 @@
|
||||
|
||||
(defcustom juvix-auto-input-method t
|
||||
"Automatically set the input method in juvix files."
|
||||
:type 'boolean
|
||||
:group 'juvix)
|
||||
|
||||
(defcustom juvix-disable-embedded-stdlib nil
|
||||
"Disable the embedded standard library."
|
||||
:type 'boolean
|
||||
:group 'juvix)
|
||||
|
||||
(defcustom juvix-stdlib-path nil
|
||||
"Specify the path to the standard library."
|
||||
:type 'directory
|
||||
:group 'juvix)
|
||||
|
||||
(provide 'juvix-customize)
|
@ -1,88 +0,0 @@
|
||||
(require 'font-lock)
|
||||
|
||||
(defgroup juvix-highlight nil
|
||||
"Syntax highlighting for Juvix."
|
||||
:group 'juvix)
|
||||
|
||||
(defgroup juvix-highlight-faces nil
|
||||
"Faces used to highlight Juvix code."
|
||||
:group 'juvix-highlight)
|
||||
|
||||
(defface juvix-highlight-keyword-face
|
||||
'((((background light))
|
||||
(:foreground "#399ee6"))
|
||||
(((background dark))
|
||||
(:foreground "#81a1c1")))
|
||||
"The face used for keywords."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-function-face
|
||||
'((((background light))
|
||||
(:foreground "#f2ae49"))
|
||||
(((background dark))
|
||||
(:foreground "#ebcb8b")))
|
||||
"The face used for functions."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-inductive-face
|
||||
'((((background light))
|
||||
(:foreground "#86b300"))
|
||||
(((background dark))
|
||||
(:foreground "#a3be8c")))
|
||||
"The face used for inductive types."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-constructor-face
|
||||
'((((background light))
|
||||
(:foreground "#a37acc"))
|
||||
(((background dark))
|
||||
(:foreground "#b48ead")))
|
||||
"The face used for constructors."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-axiom-face
|
||||
'((((background light))
|
||||
(:foreground "#f07171"))
|
||||
(((background dark))
|
||||
(:foreground "#bf616a")))
|
||||
"The face used for axioms."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-string-face
|
||||
'((((background light))
|
||||
(:foreground "#f07171"))
|
||||
(((background dark))
|
||||
(:foreground "#d08770")))
|
||||
"The face used for string literals."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-number-face
|
||||
'((((background light))
|
||||
(:foreground "#000000"))
|
||||
(((background dark))
|
||||
(:foreground "#d8dee9")))
|
||||
"The face used for numbers."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-error-face
|
||||
'((((background light))
|
||||
(:foreground "#bd3744"))
|
||||
(((background dark))
|
||||
(:foreground "#bd3744")))
|
||||
"The face used for errors."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(defface juvix-highlight-comment-face
|
||||
'((((background light))
|
||||
(:foreground "#8b2252"
|
||||
:slant italic
|
||||
))
|
||||
(((background dark))
|
||||
(:foreground "#83898d"
|
||||
:slant italic
|
||||
)
|
||||
))
|
||||
"The face used for comments."
|
||||
:group 'juvix-highlight-faces)
|
||||
|
||||
(provide 'juvix-highlight)
|
File diff suppressed because it is too large
Load Diff
@ -1,106 +0,0 @@
|
||||
(require 'juvix-customize)
|
||||
(require 'juvix-highlight)
|
||||
(require 'juvix-input)
|
||||
(require 'flycheck-juvix)
|
||||
(require 'juvix-repl)
|
||||
|
||||
(defgroup juvix nil
|
||||
"Major mode for Juvix files."
|
||||
:group 'languages)
|
||||
|
||||
(defvar juvix-mode-map
|
||||
(let ((map (make-sparse-keymap))
|
||||
(menu-map (make-sparse-keymap "Juvix")))
|
||||
(define-key map (kbd "C-c C-l") 'juvix-load)
|
||||
(define-key map (kbd "M-.") 'juvix-goto-definition)
|
||||
(define-key map (kbd "C-c C-f") 'juvix-format-buffer)
|
||||
map)
|
||||
"Keymap for Juvix mode.")
|
||||
|
||||
;;;###autoload
|
||||
(add-to-list 'auto-mode-alist '("\\.juvix\\'" . juvix-mode))
|
||||
|
||||
(defun juvix-version ()
|
||||
(let ((version (car (split-string (shell-command-to-string "juvix --version")
|
||||
"\n"))))
|
||||
(if (string-prefix-p "Juvix" version)
|
||||
version
|
||||
"Juvix")))
|
||||
|
||||
(define-derived-mode juvix-mode prog-mode (juvix-version)
|
||||
|
||||
(font-lock-mode 0)
|
||||
(when juvix-auto-input-method
|
||||
(set-input-method "juvix"))
|
||||
(setq-local comment-start "--")
|
||||
|
||||
(add-hook
|
||||
'juvix-mode-hook
|
||||
(lambda ()
|
||||
(with-eval-after-load 'evil
|
||||
(evil-define-key 'normal juvix-mode-map (kbd "SPC m l") 'juvix-load)
|
||||
(evil-define-key 'normal juvix-mode-map (kbd "SPC m g") 'juvix-goto-definition)
|
||||
(evil-define-key 'normal juvix-mode-map (kbd "SPC m f") 'juvix-format-buffer)
|
||||
(evil-define-key 'normal juvix-mode-map (kbd "g d") 'juvix-goto-definition)
|
||||
(evil-normalize-keymaps)))))
|
||||
|
||||
(defun juvix-clear-annotations ()
|
||||
"Remove all annotations from the current buffer."
|
||||
(interactive)
|
||||
(remove-list-of-text-properties (point-min) (point-max) '(face)))
|
||||
|
||||
(defun juvix-load ()
|
||||
"Load current buffer."
|
||||
(interactive)
|
||||
(save-buffer)
|
||||
(juvix-clear-annotations)
|
||||
(eval (read (shell-command-to-string
|
||||
(concat "juvix " (if juvix-disable-embedded-stdlib "--no-stdlib " "") (if juvix-stdlib-path (concat "--stdlib-path " juvix-stdlib-path " ") "") "dev highlight "
|
||||
(buffer-file-name)))))
|
||||
(save-buffer)
|
||||
(juvix-repl-load-file (buffer-file-name)))
|
||||
|
||||
(defun juvix-format-buffer ()
|
||||
"Format the current buffer."
|
||||
(interactive)
|
||||
(let ((old-point (point))
|
||||
(buff-name (buffer-file-name))
|
||||
(buff (current-buffer))
|
||||
)
|
||||
(with-temp-buffer
|
||||
(let ((
|
||||
cmd-str (concat "juvix " (if juvix-disable-embedded-stdlib "--no-stdlib " "") "dev scope "
|
||||
buff-name)
|
||||
))
|
||||
(if (zerop (call-process-shell-command
|
||||
cmd-str
|
||||
nil
|
||||
t
|
||||
))
|
||||
(progn
|
||||
(let
|
||||
((text (buffer-string)))
|
||||
(with-current-buffer buff
|
||||
(erase-buffer)
|
||||
(insert text)
|
||||
(goto-char old-point)
|
||||
(juvix-load)
|
||||
)
|
||||
)
|
||||
)
|
||||
(message "error formatting the buffer")
|
||||
)
|
||||
))))
|
||||
|
||||
(defun juvix-goto-definition ()
|
||||
"Go to the definition of the symbol at point."
|
||||
(interactive)
|
||||
(let ((goto-info (get-text-property (point) 'juvix-goto)))
|
||||
(if goto-info
|
||||
(progn
|
||||
(find-file (car goto-info))
|
||||
(juvix-load)
|
||||
(goto-char (cdr goto-info)))
|
||||
(message "No goto information found at cursor"))))
|
||||
|
||||
(provide 'juvix-mode)
|
@ -1,62 +0,0 @@
|
||||
(require 'comint)
|
||||
|
||||
(defgroup juvix-repl nil
|
||||
"Interaction mode for Juvix"
|
||||
:group 'juvix)
|
||||
|
||||
(defvar juvix-repl-program "juvix"
|
||||
"The Juvix program.")
|
||||
|
||||
(defvar juvix-repl-program-args '("repl")
|
||||
"The argument to pass to Juvix to launch the REPL.")
|
||||
|
||||
(defvar juvix-repl-mode-map
|
||||
(nconc (make-sparse-keymap) comint-mode-map))
|
||||
|
||||
(defvar juvix-repl-buffer-name "*juvix-repl*"
|
||||
"The name of the buffer to use for the `juvix-repl' comint instance.")
|
||||
|
||||
(defun run-juvix-repl ()
|
||||
"Run an inferior instance of `juvix repl' inside Emacs."
|
||||
(interactive)
|
||||
(let* ((juvix-program juvix-repl-program)
|
||||
(juvix-program-args juvix-repl-program-args)
|
||||
(buffer (get-buffer-create juvix-repl-buffer-name))
|
||||
(proc-alive (comint-check-proc buffer))
|
||||
(process (get-buffer-process buffer)))
|
||||
(unless proc-alive
|
||||
(with-current-buffer buffer
|
||||
(apply 'make-comint-in-buffer "juvix-repl" buffer
|
||||
juvix-program nil juvix-program-args)
|
||||
(juvix-repl-mode)))
|
||||
(when buffer
|
||||
(pop-to-buffer buffer))))
|
||||
|
||||
(defun juvix-repl--initialize ()
|
||||
"Helper function to initalize juvix-repl."
|
||||
(setq comint-process-echoes nil))
|
||||
|
||||
(define-derived-mode juvix-repl-mode comint-mode "Juvix REPL" "Major mode for juvix-repl")
|
||||
|
||||
(add-hook 'juvix-mode-hook 'juvix-repl--initialize)
|
||||
|
||||
(defun juvix-repl-load-file (filename)
|
||||
"Load FILENAME into the juvix-repl if it is running."
|
||||
(let* ((buffer (get-buffer juvix-repl-buffer-name))
|
||||
(proc-alive (comint-check-proc buffer)))
|
||||
(when proc-alive
|
||||
(comint-simple-send juvix-repl-buffer-name (concat ":load " filename)))))
|
||||
|
||||
(defun juvix-repl-restart ()
|
||||
"Restart the juvix REPL."
|
||||
(interactive)
|
||||
(let* ((buffer (get-buffer juvix-repl-buffer-name))
|
||||
(proc-alive (comint-check-proc buffer))
|
||||
(process (get-buffer-process buffer)))
|
||||
(if proc-alive
|
||||
(progn
|
||||
(set-process-sentinel process (lambda (p e) (run-juvix-repl)))
|
||||
(kill-process process))
|
||||
(error "No juvix repl process is runnning. Use run-juvix-repl"))))
|
||||
|
||||
(provide 'juvix-repl)
|
Loading…
Reference in New Issue
Block a user