ce35f7a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Keep :set options in sync.

This change will keep tab completion for `:set`, `:help`, and parsing in sync as new options are added. Documentation has also been updated with all options.

commitce35f7a97389f733b17c7f18d7fe0ec5ef8b1d64 authorRobert Clipsham <robert@octarineparrot.com> dateMon 19 Oct 2015, 16:04 (11 years ago) parent06edf43

3 files changed+18−19

compare with master

unifiedsplit

docs/reference/repl.rst+2−1 src/Idris/Completion.hs+2−8 src/Idris/REPLParser.hs+14−10

docs/reference/repl.rst+2−1

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

128128+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

130130+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

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

132+| | | desugarnats) |

132133+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

134135+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

src/Idris/Completion.hs+2−8

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

1212import Idris.ParseHelpers(opChars)

1313import qualified Idris.ParseExpr (constants, tactics)

1414import Idris.ParseExpr (TacticArg (..))

15−import Idris.REPLParser (allHelp)

15+import Idris.REPLParser (allHelp, setOptions)

1616import Control.Monad.State.Strict

1717

1818import Data.List

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

8282

8383completeOption :: CompletionFunc Idris

8484completeOption = completeWord Nothing " \t" completeOpt

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

86− , "showimplicits"

87− , "originalerrors"

88− , "autosolve"

89− , "nobanner"

90− , "desugarnats"

91− ]

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

9286

9387completeConsoleWidth :: CompletionFunc Idris

9488completeConsoleWidth = 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

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

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

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

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

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

3434

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+

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

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

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

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

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

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

8292 , 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 ++ ")"

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

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

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

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

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

101111 , cmd_pprint)

102112 ]

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

103114

104115parserCommands =

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

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

253264

254265 where

255266 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

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

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

264268

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

266270proofArg cmd name = do