Emacs mode and VSCode extension tutorials

docs/org/quick-start.org

@@ -6,7 +6,7 @@
 </a>
 #+end_html
 
-To install Juvix, follow the instruction in the [[./howto/installing.md][Installation How-to]].
+To install Juvix, follow the instructions in the [[./howto/installing.md][Installation How-to]].
 
 After installation, run =juvix --help= to see the list of commands.
 

docs/org/tutorials/emacs.org

@@ -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

docs/org/tutorials/learn.org

@@ -407,7 +407,7 @@ The first argument of =go= is an /accumulator/ which holds the sum computed so f
 # #+end_example
 # introduces a recursive function =go= with =n= accumulators =acc1=, ..., =accn= and further =k= arguments of the lambda expression (above =n = k = 1=). The value of the entire expression is =go v1 ... vn=. The scope of =go= is the lambda expression, i.e., it is not visible outside of it.
 
-Most imperative loops may be translated into tail recursive functional programs by converting the locally modified variables into accumulators and the loop condition into pattern matching. For example, here is a pseudocode for computing the nth Fibonacci number in linear time. The variables =cur= and =next= hold the last two computed Fibonacci numbers.
+Most imperative loops may be translated into tail recursive functional programs by converting the locally modified variables into accumulators and the loop condition into pattern matching. For example, here is an imperative pseudocode for computing the nth Fibonacci number in linear time. The variables =cur= and =next= hold the last two computed Fibonacci numbers.
 #+begin_example
 var cur : Nat := 0;
 var next : Nat := 1;

docs/org/tutorials/vscode.org

@@ -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.