mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 20:22:34 +03:00
Enable Namespace.(.field).
This commit is contained in:
parent
b745ec0e8b
commit
32de5f0966
@ -103,8 +103,7 @@ continueWith indents req
|
||||
|
||||
iOperator : Rule Name
|
||||
iOperator
|
||||
= do n <- operator
|
||||
pure (UN n)
|
||||
= operator
|
||||
<|> do symbol "`"
|
||||
n <- name
|
||||
symbol "`"
|
||||
|
@ -315,14 +315,14 @@ pragma n =
|
||||
_ => Nothing)
|
||||
|
||||
export
|
||||
operator : Rule String
|
||||
operator : Rule Name
|
||||
operator
|
||||
= terminal "Expected operator"
|
||||
(\x => case tok x of
|
||||
Symbol s =>
|
||||
if s `elem` reservedSymbols
|
||||
then Nothing
|
||||
else Just s
|
||||
else Just (UN s)
|
||||
_ => Nothing)
|
||||
|
||||
identPart : Rule String
|
||||
@ -378,18 +378,14 @@ name = opNonNS <|> do
|
||||
else pure $ NS xs (UN x)
|
||||
|
||||
opNonNS : Rule Name
|
||||
opNonNS = do
|
||||
symbol "("
|
||||
op <- operator
|
||||
symbol ")"
|
||||
pure (UN op)
|
||||
opNonNS = symbol "(" *> operator <* symbol ")"
|
||||
|
||||
opNS : List String -> Rule Name
|
||||
opNS ns = do
|
||||
symbol ".("
|
||||
op <- operator
|
||||
n <- (operator <|> recField)
|
||||
symbol ")"
|
||||
pure $ NS ns (UN op)
|
||||
pure (NS ns n)
|
||||
|
||||
export
|
||||
IndentInfo : Type
|
||||
|
Loading…
Reference in New Issue
Block a user