Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Emacs mode and VSCode extension tutorials
- Loading branch information
Showing
4 changed files
with
120 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,78 @@ | ||
* Juvix Emacs mode tutorial | ||
|
||
First, follow the instructions in the [[../reference/tooling/emacs.md][Emacs Mode Reference]] to install | ||
the Juvix Emacs mode. Once you've successfully set it up, create a | ||
file =Hello.juvix= with the following content. | ||
|
||
#+begin_example | ||
module Hello; | ||
|
||
open import Stdlib.Prelude; | ||
|
||
main : IO; | ||
main := printStringLn "Hello world!"; | ||
|
||
end; | ||
#+end_example | ||
|
||
Type =C-c C-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 =printStringLna= | ||
should be underlined with the error message "Symbol not in scope". | ||
|
||
#+begin_example | ||
module Hello; | ||
|
||
open import Stdlib.Prelude; | ||
|
||
main : IO; | ||
main := printStringLna "Hello world!"; | ||
|
||
end; | ||
#+end_example | ||
|
||
If error underlining doesn't work, make sure you have the =flycheck= | ||
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 | ||
=M-x flycheck-mode=. | ||
|
||
Let's extend our program with another definition. | ||
|
||
#+begin_example | ||
module Hello; | ||
|
||
open import Stdlib.Prelude; | ||
|
||
print : IO; | ||
print := printStringLn "Hello world!"; | ||
|
||
main : IO; | ||
main := print; | ||
|
||
end; | ||
#+end_example | ||
|
||
Place the cursor on the =print= call in the function clause of =main= | ||
and press =M-.=. The cursor will jump to the definition of =print= | ||
above. This also works across files and for definitions from the | ||
standard library. You can try using =M-.= to jump to the definition of | ||
=printStringLn=. | ||
|
||
One more feature of the Juvix Emacs mode is code formatting. To format | ||
the content of the current buffer, type =C-c C-f=. Here is the result. | ||
|
||
#+begin_example | ||
module Hello; | ||
open import Stdlib.Prelude; | ||
|
||
print : IO; | ||
print := printStringLn "Hello world!"; | ||
|
||
main : IO; | ||
main := print; | ||
end; | ||
#+end_example |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
* Juvix VSCode extension tutorial | ||
|
||
To install the Juvix VSCode extension, click on the "Extensions" | ||
button in the left panel and search for the "Juvix" extension by | ||
Heliax. | ||
|
||
Once you've installed the Juvix extension, you can open a Juvix | ||
file. For example, create a =Hello.juvix= file with the following | ||
content. | ||
|
||
#+begin_example | ||
module Hello; | ||
|
||
open import Stdlib.Prelude; | ||
|
||
main : IO; | ||
main := printStringLn "Hello world!"; | ||
|
||
end; | ||
#+end_example | ||
|
||
Syntax should be automatically highlighted for any file with =.juvix= | ||
extension. You can jump to the definition of an identifier by pressing | ||
F12 or control-clicking it. To apply the Juvix code formatter to the | ||
current file, use Shift+Ctrl+I. | ||
|
||
In the top right-hand corner of the editor window you should see | ||
several buttons. Hover the mouse pointer over a button to see its | ||
description. The functions of the buttons are as follows. | ||
|
||
- Load file in REPL (Shift+Alt+R). Launches the Juvix REPL in a | ||
separate window and loads the current file into it. You can then | ||
evaluate any definition from the loaded file. | ||
- Typecheck (Shift+Alt+T). Type-checks the current file. | ||
- Compile (Shift+Alt+C). Compiles the current file. The resulting | ||
native executable will be left in the directory of the file. | ||
- Run (Shift+Alt+X). Compiles and runs the current file. The output of | ||
the executable run is displayed in a separate window. | ||
- Html preview. Generates HTML documentation for the current file and | ||
displays it in a separate window. |