All tests and transcripts passing

This commit is contained in:
Paul Chiusano 2020-11-19 14:05:07 -05:00
parent a606fba006
commit 0a5c9bb648
3 changed files with 19 additions and 25 deletions

View File

@ -108,7 +108,10 @@ pos = do
-- successful parse, and also takes care of emitting layout tokens
-- (such as virtual semicolons and closing tokens).
token' :: (a -> Pos -> Pos -> [Token Lexeme]) -> P a -> P [Token Lexeme]
token' tok p = LP.lexeme space $ do
token' tok p = LP.lexeme space (token'' tok p)
token'' :: (a -> Pos -> Pos -> [Token Lexeme]) -> P a -> P [Token Lexeme]
token'' tok p = do
start <- pos
-- We save the current state so we can backtrack the state if `p` fails.
env <- S.get
@ -219,10 +222,9 @@ lexemes = P.optional space >> do
tok p = do start <- pos; a <- p; stop <- pos; pure [Token a start stop]
doc :: P [Token Lexeme]
doc = open <+> (CP.space *> fmap merge body) <+> close' where
open = tok (Open <$> lit "[:")
doc = open <+> (CP.space *> fmap merge body) <+> (close <* space) where
open = token'' (\t _ _ -> t) $ tok (Open <$> lit "[:")
close = tok (Close <$ lit ":]")
close' = token' (\ts _ _ -> ts) close -- consumes trailing spaces, comments
at = lit "@"
back = (Textual ":]" <$ lit "\\:]") <|> (Textual "@" <$ lit "\\@")
merge [] = []
@ -239,13 +241,14 @@ lexemes = P.optional space >> do
txt = tok (Textual <$> P.manyTill CP.anyChar (P.lookAhead sep))
sep = void at <|> void back <|> void close
backk = tok back <+> body
ref = at *> (tok wordyId <|> tok symbolyId)
ref = at *> (tok wordyId <|> tok symbolyId <|> docTyp)
atk = (ref <|> docTyp) <+> body
docTyp = do
_ <- lit "["
typ <- tok (P.manyTill CP.anyChar (P.lookAhead (lit "]")))
_ <- lit "]" *> CP.space
pure $ fmap Reserved <$> typ
t <- tok wordyId <|> tok symbolyId
pure $ (fmap Reserved <$> typ) <> t
blank = separated wordySep $
char '_' *> P.optional wordyIdSeg <&> (Blank . fromMaybe "")

View File

@ -82,11 +82,9 @@ commented = [:
commented : Doc
commented =
[:
example:
[: example:
-- a comment
f x = x + 1
-- a comment f x = x + 1
:]
```
@ -291,8 +289,7 @@ doc6 = [:
doc6 : Doc
doc6 =
[:
- foo
[: - foo
- bar
and the rest.
:]
@ -382,9 +379,8 @@ para line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolo
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 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
@ -491,8 +487,7 @@ View is fine.
test2 : Doc
test2 =
[:
Take a look at this:
[: Take a look at this:
@[source] foo ▶ bar
:]
@ -501,7 +496,6 @@ But note it's not obvious how display should best be handling this. At the mome
```ucm
.> display test2
Take a look at this:
foo n =
use Nat +

View File

@ -140,7 +140,6 @@ Now that documentation is linked to the definition. We can view it if we like:
.> display 1
`builtin.List.take n xs` returns the first `n` elements of `xs`.
(No need to add line breaks manually. The display command will
do wrapping of text for you. Indent any lines where you don't
@ -164,7 +163,6 @@ Or there's also a convenient function, `docs`, which shows the `Doc` values that
```ucm
.> docs builtin.List.take
`builtin.List.take n xs` returns the first `n` elements of `xs`.
(No need to add line breaks manually. The display command will
do wrapping of text for you. Indent any lines where you don't
@ -190,11 +188,10 @@ Note that if we view the source of the documentation, the various references are
docs.List.take : Doc
docs.List.take =
[:
`@builtin.List.take n xs` returns the first `n` elements of `xs`.
(No need to add line breaks manually. The display command will
do wrapping of text for you. Indent any lines where you don't
want it to do this.)
[: `@builtin.List.take n xs` returns the first `n` elements of
`xs`. (No need to add line breaks manually. The display command
will do wrapping of text for you. Indent any lines where you
don't want it to do this.)
## Examples: