ce35f7a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Keep :set options in sync.

ce35f7aRobert Clipsham11 years ago

docs/reference/repl.rst+2−1

@@ -128,7 +128,8 @@ The current set of supported commands are:

128+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

129|:? :h :help | | Display this help text |

130+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

131−|:set | <option> | Set an option (errorcontext, showimplicits) |

131+|:set | <option> | Set an option (errorcontext, showimplicits, originalerrors, autosolve, nobanner, warnreach, evaltypes, |

132+| | | desugarnats) |

132+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

133+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

133|:unset | <option> | Unset an option |

134|:unset | <option> | Unset an option |

134+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

135+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

src/Idris/Completion.hs+2−8

@@ -12,7 +12,7 @@ import Idris.Colours

12import Idris.ParseHelpers(opChars)

13import qualified Idris.ParseExpr (constants, tactics)

14import Idris.ParseExpr (TacticArg (..))

15−import Idris.REPLParser (allHelp)

15+import Idris.REPLParser (allHelp, setOptions)

16import Control.Monad.State.Strict

18import Data.List

@@ -82,13 +82,7 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

83completeOption :: CompletionFunc Idris

84completeOption = completeWord Nothing " \t" completeOpt

85− where completeOpt = return . completeWith [ "errorcontext"

85+ where completeOpt = return . completeWith (map fst setOptions)

86− , "showimplicits"

87− , "originalerrors"

88− , "autosolve"

89− , "nobanner"

90− , "desugarnats"

91− ]

93completeConsoleWidth :: CompletionFunc Idris

87completeConsoleWidth :: CompletionFunc Idris

94completeConsoleWidth = completeWord Nothing " \t" completeW

88completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/REPLParser.hs+14−10

@@ -1,5 +1,5 @@

2−module Idris.REPLParser (parseCmd, help, allHelp) where

2+module Idris.REPLParser (parseCmd, help, allHelp, setOptions) where

4import System.FilePath ((</>))

5import System.Console.ANSI (Color(..))

@@ -32,6 +32,16 @@ parseCmd i inputname = P.runparser pCmd i inputname . trim

32type CommandTable = [ ( [String], CmdArg, String

33 , String -> P.IdrisParser (Either String Command) ) ]

35+setOptions :: [(String, Opt)]

36+setOptions = [("errorcontext", ErrContext),

37+ ("showimplicits", ShowImpl),

38+ ("originalerrors", ShowOrigErr),

39+ ("autosolve", AutoSolve),

40+ ("nobanner", NoBanner),

41+ ("warnreach", WarnReach),

42+ ("evaltypes", EvalTypes),

43+ ("desugarnats", DesugarNats)]

44+

35help :: [([String], CmdArg, String)]

45help :: [([String], CmdArg, String)]

36help = (["<expr>"], NoArg, "Evaluate an expression") :

46help = (["<expr>"], NoArg, "Evaluate an expression") :

37 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

47 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

@@ -80,7 +90,7 @@ parserCommandsForHelp =

80 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

90 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

81 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

91 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

82 , noArgCmd ["?", "h", "help"] Help "Display this help text"

92 , noArgCmd ["?", "h", "help"] Help "Display this help text"

83− , optArgCmd ["set"] SetOpt "Set an option (errorcontext, showimplicits)"

93+ , optArgCmd ["set"] SetOpt $ "Set an option (" ++ optionsList ++ ")"

84 , optArgCmd ["unset"] UnsetOpt "Unset an option"

94 , optArgCmd ["unset"] UnsetOpt "Unset an option"

85 , (["color", "colour"], ColourArg

95 , (["color", "colour"], ColourArg

86 , "Turn REPL colours on or off; set a specific colour"

96 , "Turn REPL colours on or off; set a specific colour"

@@ -100,6 +110,7 @@ parserCommandsForHelp =

100 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

110 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

101 , cmd_pprint)

111 , cmd_pprint)

102 ]

112 ]

113+ where optionsList = intercalate ", " $ map fst setOptions

103

114

104parserCommands =

115parserCommands =

105 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

116 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

@@ -253,14 +264,7 @@ optArg cmd name = do

253

264

254 where

265 where

255 pOption :: P.IdrisParser Opt

266 pOption :: P.IdrisParser Opt

256− pOption = do discard (P.symbol "errorcontext"); return ErrContext

257− <|> do discard (P.symbol "showimplicits"); return ShowImpl

258− <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

259− <|> do discard (P.symbol "autosolve"); return AutoSolve

260− <|> do discard (P.symbol "nobanner") ; return NoBanner

261− <|> do discard (P.symbol "warnreach"); return WarnReach

262− <|> do discard (P.symbol "evaltypes"); return EvalTypes

267+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

263− <|> do discard (P.symbol "desugarnats"); return DesugarNats

264

268

265proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

269proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

266proofArg cmd name = do

270proofArg cmd name = do