idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 20:42:13 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #198 from edwinb/path-fix

Browse Source 
Allow parsing multiple separators in Path
This commit is contained in:
Edwin Brady 2020-05-30 11:38:25 +01:00 committed by GitHub
commit 5fd0f77f4e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/contrib/System/Path.idr
View File

@ -395,9 +395,9 @@ parseBody = do text <- match PTText
private
parsePath : Grammar PathToken False Path
parsePath = do vol <- optional parseVolumn
root <- optional bodySeparator
body <- sepBy bodySeparator parseBody
trailSep <- optional bodySeparator
root <- optional (some bodySeparator)
body <- sepBy (some bodySeparator) parseBody
trailSep <- optional (some bodySeparator)
pure $ MkPath vol (isJust root) body (isJust trailSep)
||| Attempt to parse a String into Path.

2
src/Idris/ModTree.idr
View File

@ -231,7 +231,7 @@ buildDeps fname
clearCtxt; addPrimitives
put MD initMetadata
mainttc <- getTTCFileName fname ".ttc"
log 10 $ "Reloading " ++ show mainttc
log 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
readAsMain mainttc
-- Load the associated metadata for interactive editing

6
src/Utils/Path.idr
View File

@ -212,9 +212,9 @@ parseBody = do text <- match PTText
parsePath : Grammar PathToken False Path
parsePath = do vol <- optional parseVolume
root <- optional bodySeparator
body <- sepBy bodySeparator parseBody
trailSep <- optional bodySeparator
root <- optional (some bodySeparator)
body <- sepBy (some bodySeparator) parseBody
trailSep <- optional (some bodySeparator)
let body = filter (\case Normal s => ltrim s /= ""
_ => True) body
pure $ MkPath vol (isJust root) body (isJust trailSep)