git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2759 from jeremy-w/jeremy-w/improve-filename-error-messages
9963bbeNiklas Larsson
CHANGELOG+4
compare with master
unifiedsplit
@@ -45,6 +45,10 @@ Tool updates
45* iPKG files have a new option `pkgs` which takes a comma-separated list
45* iPKG files have a new option `pkgs` which takes a comma-separated list
46 of package names that the idris project depends on. This reduces bloat
46 of package names that the idris project depends on. This reduces bloat
47 in the `opts` option with multiple package declarations.
47 in the `opts` option with multiple package declarations.
48+* iPKG files now allow `executable = "your filename here"` in addition to
49+ the existing `executable = yourFilenameHere` style. While the unquoted
50+ version is limited to filenames that look like namespaced Idris identifiers
51+ (`your.filename.here`), the quoted version accepts any valid filename.
48* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now
52* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now
49 adds missing clauses if there is already a definition.
53 adds missing clauses if there is already a definition.
50
54
src/Pkg/PParser.hs+24−9
@@ -15,6 +15,7 @@ import Idris.CmdOptions
15import Control.Monad.State.Strict
15import Control.Monad.State.Strict
16import Control.Applicative
16import Control.Applicative
17import System.FilePath (takeFileName, isValid)
17import System.FilePath (takeFileName, isValid)
18+import Data.Maybe (isNothing, fromJust)
18
19
19import Util.System
20import Util.System
20
21
@@ -79,18 +80,32 @@ filename = (do
79 -- Through at least version 0.9.19.1, IPKG executable values were
80 -- Through at least version 0.9.19.1, IPKG executable values were
80 -- possibly namespaced identifiers, like foo.bar.baz.
81 -- possibly namespaced identifiers, like foo.bar.baz.
81 show <$> fst <$> iName []
82 show <$> fst <$> iName []
82− if isValidFilename filename
83+ case filenameErrorMessage filename of
83− then return filename
84+ Just errorMessage -> fail errorMessage
84− else fail "a filename must be non-empty and have no directory component")
85+ Nothing -> return filename)
85 <?> "filename"
86 <?> "filename"
86 where
87 where
87− isValidFilename :: FilePath -> Bool
88+ -- TODO: Report failing span better! We could lookAhead,
88− isValidFilename path =
89+ -- or do something with DeltaParsing?
89− and [isNonEmpty, isValidPath, hasNoDirectoryComponent]
90+ filenameErrorMessage :: FilePath -> Maybe String
91+ filenameErrorMessage path = either Just (const Nothing) $ do
92+ checkEmpty path
93+ checkValid path
94+ checkNoDirectoryComponent path
90 where
95 where
91− isNonEmpty = path /= ""
96+ checkThat ok message =
97+ if ok then Right () else Left message
98+
99+ checkEmpty path =
100+ checkThat (path /= "") "filename must not be empty"
101+
102+ checkValid path =
92− isValidPath = System.FilePath.isValid path
103+ checkThat (System.FilePath.isValid path)
104+ "filename must contain only valid characters"
105+
106+ checkNoDirectoryComponent path =
93− hasNoDirectoryComponent = path == takeFileName path
107+ checkThat (path == takeFileName path)
108+ "filename must contain no directory component"
94
109
95
110
96pClause :: PParser ()
111pClause :: PParser ()
test/pkg003/run+1−1
@@ -3,4 +3,4 @@
3### containing a valid filename.
3### containing a valid filename.
4idris $@ --build test.ipkg
4idris $@ --build test.ipkg
5rm -f *.ibc
5rm -f *.ibc
6−rm -f 'quoting-allows-hyphens and spaces? and fun stuff!'
6+rm -f 'quoting-allows-hyphens and spaces and fun stuff!'
test/pkg004/expected+4−5
@@ -1,6 +1,5 @@
1−Uncaught error: user error (test.ipkg:10:1: error: a
1+Uncaught error: user error (test.ipkg:10:1: error: filename
2− filename must be non-empty and
3− have no directory
2+ must contain no directory
4 component, expected: space
3 component, expected: space
5−<EOF>
4+<EOF>
6−^ )
5+^ )