When flattening the `SimpleDocTree` created from a `SimpleDocStream`, the
first part of a concatenated doc was sometimes dropped, depending on the
result of the recursive call to `flatten`.
Previously, parameter block reused the same syntax as in Idris1:
```
parameters (v1 : t1, … , vn : tn)
```
Unfortunately this syntax presents some issues:
- It does not allow to declare implicit parameters
- It does not allow to specify which multiplicity to use
- It is inconsistent with the syntax used for named arguments elsewhere
in the language.
This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:
```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```
It also enables other features like multiple declarations of arguments
with the same type:
```
parameters (v1, v2 : Type)
```
The previous names were a holdover from when these functions were a part
of `RefC.compileExpr`. The new names more accurately reflect their usage
in this context.
On Unix-like operating systems stdio.h is usually line-buffered. As
putStr uses fputs(3) from stdio.h internally, output will be written to
standard out after a newline character is written to the buffer. Since
the prompt does not contain a newline, it will only be written to
standard output after the user presses return. I encountered this issue
on Alpine Linux which uses musl libc (instead of glibc). However, I
believe this issue is likely also reproducible with glibc. This commit
fixes this issue by flushing standard output after writing the prompt to
it. Surprisingly, `src/Idris/IDEMode/REPL.idr` already does this
correctly, `src/Idris/REPL.idr` does not though.
If they're big, they take a long time to instantiate, and if they
consist of a lot of functions, chances are that normalising them will
make them much smaller. This significantly improves type checking
performance for some programs with lots of type level computation going
on.
The threshold is set with %nf_metavar_threshold, but the default value
of 50 is probably fine. Set it to 0 to always normalise metavar
solutions, or something higher than 1000 to essentially never do it.
It's roughly a count of nodes in the typechecked syntax tree under the
first function application.
