Juvix Emacs mode tutorial¶
First, follow the instructions in the Emacs Mode
Reference to install the Juvix Emacs
mode. Once you've successfully set it up, create a file
with the following content.
-- HelloWorld.juvix module HelloWorld; open import Stdlib.Prelude; main : IO; main := printStringLn "hello world!";
Type Ctrl+C+Ctrl+L to run the scoper and highlight the syntax.
If you make a mistake in your program, it is automatically underlined in red with the error message popping up when you hover the mouse pointer over the underlined part.
For example, in the following program the identifier
should be underlined with the error message "Symbol not in scope".
module Hello; open import Stdlib.Prelude; main : IO; main := printStringLna "Hello world!"; end;
If error underlining doesn't work, make sure you have the
mode turned on. It should be turned on automatically when loading
juvix-mode, but in case this doesn't work you can enable it with
Let's extend our program with another definition.
module Hello; open import Stdlib.Prelude; print : IO; print := printStringLn "Hello world!"; main : IO; main := print; end;
Place the cursor on the
M-.. The cursor will jump to the definition of
M-. to jump to the definition of
One more feature of the Juvix Emacs mode is code formatting. To format the content of the current buffer, type Ctrl+C+Ctrl+F.