mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-01 16:12:26 +03:00
Add 'tryParse' function to 'System.Path' (#2234)
This commit is contained in:
parent
266e06cab7
commit
f016a81e37
@ -244,6 +244,13 @@ parsePath =
|
||||
(x::xs) => x :: delete CurDir xs
|
||||
pure $ MkPath vol (isJust root) body (isJust trailSep)
|
||||
|
||||
export
|
||||
tryParse : String -> Maybe Path
|
||||
tryParse str =
|
||||
case parse parsePath (lexPath str) of
|
||||
Right (path, []) => Just path
|
||||
_ => Nothing
|
||||
|
||||
||| Parses a String into Path.
|
||||
|||
|
||||
||| The string is parsed as much as possible from left to right, and the invalid
|
||||
|
Loading…
Reference in New Issue
Block a user