You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Doc comments annotate the following atom, usually some kind of a definition:
||| This is a doc comment.
def(bar, ..., ...)
Right now these are discarded in the lexer. Instead they should either be saved as a token, or stored as part of the following token. Importantly, multiple doc comment lines ought to be combined (while preserving the lines), e.g.
||| Line 1 of doc comment
||| Line 2 of doc comment
def(my-word, ..., ...)
The text was updated successfully, but these errors were encountered:
Doc comments annotate the following atom, usually some kind of a definition:
Right now these are discarded in the lexer. Instead they should either be saved as a token, or stored as part of the following token. Importantly, multiple doc comment lines ought to be combined (while preserving the lines), e.g.
The text was updated successfully, but these errors were encountered: