@@ -30,7 +30,8 @@ import Paths_idris
3030-- on with the REPL.
3131
3232data Opt = Filename String
33− | Version
33+ | Ver
34+ | Usage
3435 | NoPrelude
3536 | NoREPL
3637 | OLogging Int
@@ -48,6 +49,8 @@ runIdris opts =
4849 do let inputs = opt getFile opts
4950 let runrepl = not (NoREPL `elem` opts)
5051 let output = opt getOutput opts
52+ when (Ver `elem` opts) $ lift showver
53+ when (Usage `elem` opts) $ lift usage
5154 setREPL runrepl
5255 mapM_ makeOption opts
5356 elabPrims
@@ -80,8 +83,11 @@ getOutput _ = Nothing
8083opt :: (Opt -> Maybe a) -> [Opt] -> [a]
8184opt = mapMaybe
8285
83−usage = do putStrLn "You're doing it wrong"
84− exitWith (ExitFailure 1)
86+usage = do putStrLn usagemsg
87+ exitWith ExitSuccess
88+
89+showver = do putStrLn $ "Idris version " ++ ver
90+ exitWith ExitSuccess
8591
8692parseArgs :: [String] -> IO [Opt]
8793parseArgs [] = return []
@@ -91,22 +97,10 @@ parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
9197parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
9298parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
9399parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
100+parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
101+parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
94102parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
95103
96−{-
97−main'
98− = do f <- readFile "test.mi"
99− case parseFile f of
100− Left err -> print err
101− Right defs -> do
102− print defs
103− case checkProgram emptyContext defs of
104− OK ctxt -> do print (toAlist ctxt)
105− runShell (initState ctxt)
106− return ()
107− err -> print err
108− -}
109−
110104ver = showVersion version
111105
112106banner = " ____ __ _ \n" ++
@@ -115,3 +109,13 @@ banner = " ____ __ _ \n" ++
115109 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
116110 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
117111
112+usagemsg = "Idris version " ++ ver ++ "\n" ++
113+ "--------------" ++ map (\x -> '-') ver ++ "\n" ++
114+ "Usage: idris [input file] [options]\n" ++
115+ "Options:\n" ++
116+ "\t--check Type check only\n" ++
117+ "\t-o [file] Generate executable\n" ++
118+ "\t--noprelude Don't import the prelude\n" ++
119+ "\t--typeintype Disable universe checking\n" ++
120+ "\t--log [level] Set debugging log level\n"
121+