[ REPL ] Added commands :ti and :opts (#1241)

:ti does the same thing as :t, but shows the type as if showimplicits
were set. The value of REPLOpt.ShowImplicits is unchanged.

:opts shows the current values of the options that can be set or unset
with :set/:unset. (This already existed in REPLCmd.GetOpts, idk why it
just wasn't in Parser.parserCommandsForHelp.)

Also fixed the spacing of the help message.

src/Idris/Parser.idr

@@ -1863,6 +1863,7 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
 parserCommandsForHelp : CommandTable
 parserCommandsForHelp =
   [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
+  , exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits "Check the type of an expression, showing implicit arguments"
   , nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
   , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch "Search for values by type"
   , nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
@@ -1873,6 +1874,7 @@ parserCommandsForHelp =
   , stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand "Run a shell command"
   , optArgCmd (ParseIdentCmd "set") SetOpt True "Set an option"
   , optArgCmd (ParseIdentCmd "unset") SetOpt False "Unset an option"
+  , noArgCmd (ParseREPLCmd ["opts"]) GetOpts "Show current options settings"
   , compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile "Compile to an executable"
   , exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
   , stringArgCmd (ParseIdentCmd "directive") CGDirective "Set a codegen-specific directive"

src/Idris/REPL.idr

@@ -722,6 +722,12 @@ process (Check itm)
          ty <- getTerm gty
          ity <- resugar [] !(normaliseScope defs [] ty)
          pure (TermChecked itm ity)
+process (CheckWithImplicits itm)
+    = do showImplicits <- showImplicits <$> getPPrint
+         setOpt (ShowImplicits True)
+         result <- process (Check itm)
+         setOpt (ShowImplicits showImplicits)
+         pure result
 process (PrintDef fn)
     = do defs <- get Ctxt
          case !(lookupCtxtName fn (gamma defs)) of
@@ -1074,7 +1080,7 @@ mutual
         m ++ (makeSpace $ c2 `minus` length m) ++ r
 
       cmdInfo : (List String, CmdArg, String) -> String
-      cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
+      cmdInfo (cmds, args, text) = " " ++ col 18 20 (showSep " " cmds) (show args) text
 
   export
   displayErrors : {auto c : Ref Ctxt Defs} ->

src/Idris/Syntax.idr

@@ -446,6 +446,7 @@ data REPLCmd : Type where
      NewDefn : List PDecl -> REPLCmd
      Eval : PTerm -> REPLCmd
      Check : PTerm -> REPLCmd
+     CheckWithImplicits : PTerm -> REPLCmd
      PrintDef : Name -> REPLCmd
      Reload : REPLCmd
      Load : String -> REPLCmd