@@ -10,10 +10,50 @@ import Options.Applicative
1010import Options.Applicative.Arrows
1111import Data.Maybe
1212
13+import qualified Text.PrettyPrint.ANSI.Leijen as PP
14+
1315runArgParser :: IO [Opt]
14−runArgParser = do opts <- execParser $ info parser $
15− header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")
16+runArgParser = do opts <- execParser $ info parser
17+ (fullDesc
18+ <> headerDoc (Just idrisHeader)
19+ <> progDescDoc (Just idrisProgDesc)
20+ <> footerDoc (Just idrisFooter)
21+ )
1622 return $ preProcOpts opts []
23+ where
24+ idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]
25+ idrisProgDesc = PP.vsep [PP.text "Idris is a general purpose pure functional programming language with dependent",
26+ PP.text "types. Dependent types allow types to be predicated on values, meaning that",
27+ PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",
28+ PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
29+ PP.text "and ML.",
30+ PP.empty,
31+ PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [
32+ "+ Full dependent types with dependent pattern matching",
33+ "+ where clauses, with rule, simple case expressions",
34+ "+ pattern matching let and lambda bindings",
35+ "+ Type classes, monad comprehensions",
36+ "+ do notation, idiom brackets",
37+ "+ syntactic conveniences for lists, tuples, dependent pairs",
38+ "+ Totality checking",
39+ "+ Coinductive types",
40+ "+ Indentation significant syntax, extensible syntax",
41+ "+ Tactic based theorem proving (influenced by Coq)",
42+ "+ Cumulative universes",
43+ "+ Simple foreign function interface (to C)",
44+ "+ Hugs style interactive environment"
45+ ],
46+ PP.empty]
47+ idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",
48+ PP.text "and project. Thus the tooling provided and resulting programs created",
49+ PP.text "should not necessarily be seen as production ready nor for industrial use.",
50+ PP.empty,
51+ PP.text "More details over Idris can be found online here:",
52+ PP.empty,
53+ PP.indent 4 (PP.text "http://www.idris-lang.org/")]
54+
55+
56+
1757
1858pureArgParser :: [String] -> [Opt]
1959pureArgParser args = case execParserMaybe (info parser idm) args of