mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
0031542faf
This is for consistency with the `cmark` style. Now the blocks we still pretty-print ourselves will match the bulk of them that `cmark` produces.
538 lines
13 KiB
Markdown
538 lines
13 KiB
Markdown
This transcript explains a few minor details about doc parsing and pretty-printing, both from a user point of view and with some implementation notes. The later stuff is meant more as unit testing than for human consumption. (The ucm `add` commands and their output are hidden for brevity.)
|
|
|
|
Docs can be used as inline code comments.
|
|
|
|
``` unison
|
|
foo : Nat -> Nat
|
|
foo n =
|
|
_ = [: do the thing :]
|
|
n + 1
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
foo : Nat -> Nat
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view foo
|
|
|
|
foo : Nat -> Nat
|
|
foo n =
|
|
use Nat +
|
|
_ = [: do the thing :]
|
|
n + 1
|
|
|
|
```
|
|
Note that `@` and `:]` must be escaped within docs.
|
|
|
|
``` unison
|
|
escaping = [: Docs look [: like \@this \:] :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
escaping : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view escaping
|
|
|
|
escaping : Doc
|
|
escaping = [: Docs look [: like \@this \:] :]
|
|
|
|
```
|
|
(Alas you can't have `\@` or `\:]` in your doc, as there's currently no way to 'unescape' them.)
|
|
|
|
``` unison
|
|
-- Note that -- comments are preserved within doc literals.
|
|
commented = [:
|
|
example:
|
|
|
|
-- a comment
|
|
f x = x + 1
|
|
:]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
commented : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view commented
|
|
|
|
commented : Doc
|
|
commented =
|
|
[: example:
|
|
|
|
-- a comment f x = x + 1
|
|
:]
|
|
|
|
```
|
|
### Indenting, and paragraph reflow
|
|
|
|
Handling of indenting in docs between the parser and pretty-printer is a bit fiddly.
|
|
|
|
``` unison
|
|
-- The leading and trailing spaces are stripped from the stored Doc by the
|
|
-- lexer, and one leading and trailing space is inserted again on view/edit
|
|
-- by the pretty-printer.
|
|
doc1 = [: hi :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc1 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc1
|
|
|
|
doc1 : Doc
|
|
doc1 = [: hi :]
|
|
|
|
```
|
|
``` unison
|
|
-- Lines (apart from the first line, i.e. the bit between the [: and the
|
|
-- first newline) are unindented until at least one of
|
|
-- them hits the left margin (by a post-processing step in the parser).
|
|
-- You may not notice this because the pretty-printer indents them again on
|
|
-- view/edit.
|
|
doc2 = [: hello
|
|
- foo
|
|
- bar
|
|
and the rest. :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc2 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc2
|
|
|
|
doc2 : Doc
|
|
doc2 =
|
|
[: hello
|
|
- foo
|
|
- bar
|
|
and the rest. :]
|
|
|
|
```
|
|
``` unison
|
|
doc3 = [: When Unison identifies a paragraph, it removes any newlines from it before storing it, and then reflows the paragraph text to fit the display window on display/view/edit.
|
|
|
|
For these purposes, a paragraph is any sequence of non-empty lines that have zero indent (after the unindenting mentioned above.)
|
|
|
|
- So this is not a paragraph, even
|
|
though you might want it to be.
|
|
|
|
And this text | as a paragraph
|
|
is not treated | either.
|
|
|
|
Note that because of the special treatment of the first line mentioned above, where its leading space is removed, it is always treated as a paragraph.
|
|
:]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc3 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc3
|
|
|
|
doc3 : Doc
|
|
doc3 =
|
|
[: When Unison identifies a paragraph, it removes any
|
|
newlines from it before storing it, and then reflows the
|
|
paragraph text to fit the display window on
|
|
display/view/edit.
|
|
|
|
For these purposes, a paragraph is any sequence of non-empty
|
|
lines that have zero indent (after the unindenting mentioned
|
|
above.)
|
|
|
|
- So this is not a paragraph, even
|
|
though you might want it to be.
|
|
|
|
And this text | as a paragraph
|
|
is not treated | either.
|
|
|
|
Note that because of the special treatment of the first line
|
|
mentioned above, where its leading space is removed, it is
|
|
always treated as a paragraph.
|
|
:]
|
|
|
|
```
|
|
``` unison
|
|
doc4 = [: Here's another example of some paragraphs.
|
|
|
|
All these lines have zero indent.
|
|
|
|
- Apart from this one. :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc4 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc4
|
|
|
|
doc4 : Doc
|
|
doc4 =
|
|
[: Here's another example of some paragraphs.
|
|
|
|
All these lines have zero indent.
|
|
|
|
- Apart from this one. :]
|
|
|
|
```
|
|
``` unison
|
|
-- The special treatment of the first line does mean that the following
|
|
-- is pretty-printed not so prettily. To fix that we'd need to get the
|
|
-- lexer to help out with interpreting doc literal indentation (because
|
|
-- it knows what columns the `[:` was in.)
|
|
doc5 = [: - foo
|
|
- bar
|
|
and the rest. :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc5 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc5
|
|
|
|
doc5 : Doc
|
|
doc5 =
|
|
[: - foo
|
|
- bar
|
|
and the rest. :]
|
|
|
|
```
|
|
``` unison
|
|
-- You can do the following to avoid that problem.
|
|
doc6 = [:
|
|
- foo
|
|
- bar
|
|
and the rest.
|
|
:]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
doc6 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view doc6
|
|
|
|
doc6 : Doc
|
|
doc6 =
|
|
[: - foo
|
|
- bar
|
|
and the rest.
|
|
:]
|
|
|
|
```
|
|
### More testing
|
|
|
|
``` unison
|
|
-- Check empty doc works.
|
|
empty = [::]
|
|
|
|
expr = foo 1
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
empty : Doc
|
|
expr : Nat
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view empty
|
|
|
|
empty : Doc
|
|
empty = [: :]
|
|
|
|
```
|
|
``` unison
|
|
test1 = [:
|
|
The internal logic starts to get hairy when you use the \@ features, for example referencing a name like @List.take. Internally, the text between each such usage is its own blob (blob ends here --> @List.take), so paragraph reflow has to be aware of multiple blobs to do paragraph reflow (or, more accurately, to do the normalization step where newlines with a paragraph are removed.)
|
|
|
|
Para to reflow: lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor ending in ref @List.take
|
|
|
|
@List.take starting para lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
Middle of para: lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor @List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
- non-para line (@List.take) with ref @List.take
|
|
Another non-para line
|
|
@List.take starting non-para line
|
|
|
|
- non-para line with ref @List.take
|
|
before a para-line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
- non-para line followed by a para line starting with ref
|
|
@List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
a para-line ending with ref lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor @List.take
|
|
- non-para line
|
|
|
|
para line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
|
@List.take followed by non-para line starting with ref.
|
|
|
|
@[signature] List.take
|
|
|
|
@[source] foo
|
|
|
|
@[evaluate] expr
|
|
|
|
@[include] doc1
|
|
|
|
-- note the leading space below
|
|
@[signature] List.take
|
|
|
|
:]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
test1 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view test1
|
|
|
|
test1 : Doc
|
|
test1 =
|
|
[: The internal logic starts to get hairy when you use the
|
|
\@ features, for example referencing a name like @List.take.
|
|
Internally, the text between each such usage is its own blob
|
|
(blob ends here --> @List.take), so paragraph reflow has to
|
|
be aware of multiple blobs to do paragraph reflow (or, more
|
|
accurately, to do the normalization step where newlines with
|
|
a paragraph are removed.)
|
|
|
|
Para to reflow: lorem ipsum dolor lorem ipsum dolor lorem
|
|
ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
|
dolor lorem ipsum dolor ending in ref @List.take
|
|
|
|
@List.take starting para lorem ipsum dolor lorem ipsum dolor
|
|
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem
|
|
ipsum dolor lorem ipsum dolor.
|
|
|
|
Middle of para: lorem ipsum dolor lorem ipsum dolor lorem
|
|
ipsum dolor @List.take lorem ipsum dolor lorem ipsum dolor
|
|
lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
- non-para line (@List.take) with ref @List.take
|
|
Another non-para line
|
|
@List.take starting non-para line
|
|
|
|
- non-para line with ref @List.take
|
|
before a para-line lorem ipsum dolor lorem ipsum dolor lorem
|
|
ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
|
dolor lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
- non-para line followed by a para line starting with ref
|
|
@List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
|
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
|
lorem ipsum dolor lorem ipsum dolor.
|
|
|
|
a para-line ending with ref lorem ipsum dolor lorem ipsum
|
|
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
|
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor @List.take
|
|
- non-para line
|
|
|
|
para line lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
|
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
|
lorem ipsum dolor lorem ipsum dolor
|
|
@List.take followed by non-para line starting with ref.
|
|
|
|
@[signature] List.take
|
|
|
|
@[source] foo
|
|
|
|
@[evaluate] expr
|
|
|
|
@[include] doc1
|
|
|
|
-- note the leading space below
|
|
@[signature] List.take
|
|
|
|
:]
|
|
|
|
```
|
|
``` unison
|
|
-- Regression test for #1363 - preservation of spaces after @ directives in first line when unindenting
|
|
reg1363 = [: `@List.take foo` bar
|
|
baz :]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
reg1363 : Doc
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> view reg1363
|
|
|
|
reg1363 : Doc
|
|
reg1363 = [: `@List.take foo` bar baz :]
|
|
|
|
```
|
|
``` unison
|
|
-- Demonstrate doc display when whitespace follows a @[source] or @[evaluate]
|
|
-- whose output spans multiple lines.
|
|
|
|
test2 = [:
|
|
Take a look at this:
|
|
@[source] foo ▶ bar
|
|
:]
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
test2 : Doc
|
|
|
|
```
|
|
View is fine.
|
|
|
|
``` ucm
|
|
scratch/main> view test2
|
|
|
|
test2 : Doc
|
|
test2 =
|
|
[: Take a look at this:
|
|
@[source] foo ▶ bar
|
|
:]
|
|
|
|
```
|
|
But note it's not obvious how display should best be handling this. At the moment it just does the simplest thing:
|
|
|
|
``` ucm
|
|
scratch/main> display test2
|
|
|
|
Take a look at this:
|
|
foo : Nat -> Nat
|
|
foo n =
|
|
use Nat +
|
|
_ = [: do the thing :]
|
|
n + 1 ▶ bar
|
|
|
|
|
|
```
|