@@ -1,4 +1,4 @@
1−{-# LANGUAGE CPP #-}
1+{-# LANGUAGE CPP, ConstraintKinds #-}
22#if !(MIN_VERSION_base(4,8,0))
33{-# LANGUAGE OverlappingInstances #-}
44#endif
@@ -14,6 +14,7 @@ import Idris.CmdOptions
1414
1515import Control.Monad.State.Strict
1616import Control.Applicative
17+import System.FilePath (takeFileName, isValid)
1718
1819import Util.System
1920
@@ -62,11 +63,41 @@ pPkg = do
6263 eof
6364 return st
6465
66+
67+-- | Parses a filename.
68+-- |
69+-- | Treated for now as an identifier or a double-quoted string.
70+filename :: (MonadicParsing m, HasLastTokenSpan m) => m String
71+filename = (do
72+ filename <- token $
73+ -- Treat a double-quoted string as a filename to support spaces.
74+ -- This also moves away from tying filenames to identifiers, so
75+ -- it will also accept hyphens
76+ -- (https://github.com/idris-lang/Idris-dev/issues/2721)
77+ stringLiteral
78+ <|>
79+ -- Through at least version 0.9.19.1, IPKG executable values were
80+ -- possibly namespaced identifiers, like foo.bar.baz.
81+ show <$> fst <$> iName []
82+ if isValidFilename filename
83+ then return filename
84+ else fail "a filename must be non-empty and have no directory component")
85+ <?> "filename"
86+ where
87+ isValidFilename :: FilePath -> Bool
88+ isValidFilename path =
89+ and [isNonEmpty, isValidPath, hasNoDirectoryComponent]
90+ where
91+ isNonEmpty = path /= ""
92+ isValidPath = System.FilePath.isValid path
93+ hasNoDirectoryComponent = path == takeFileName path
94+
95+
6596pClause :: PParser ()
6697pClause = do reserved "executable"; lchar '=';
67− exec <- fst <$> iName []
98+ exec <- filename
6899 st <- get
69− put (st { execout = Just (show exec) })
100+ put (st { execout = Just exec })
70101 <|> do reserved "main"; lchar '=';
71102 main <- fst <$> iName []
72103 st <- get