Retain the --client mode behaviour

Author: Russoul

src/Idris/REPL.idr

@@ -1074,7 +1074,7 @@ mutual
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
-  displayResult (REPLError err) = printError err
+  displayResult (REPLError err) = printResult err
   displayResult (Evaluated x Nothing) = printResult $ prettyTerm x
   displayResult (Evaluated x (Just y)) = printResult (prettyTerm x <++> colon <++> prettyTerm y)
   displayResult (Printed xs) = printResult xs
@@ -1085,9 +1085,9 @@ mutual
   displayResult (ErrorLoadingModule x err) = printResult (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err))
   displayResult (ErrorLoadingFile x err) = printResult (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
   displayResult (ErrorsBuildingFile x errs) = printResult (reflow "Error(s) building file" <++> pretty x) -- messages already displayed while building
-  displayResult NoFileLoaded = printError (reflow "No file can be reloaded")
+  displayResult NoFileLoaded = printResult (reflow "No file can be reloaded")
   displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> dquotes (pretty dir))
-  displayResult CompilationFailed = printError (reflow "Compilation failed")
+  displayResult CompilationFailed = printResult (reflow "Compilation failed")
   displayResult (Compiled f) = printResult (pretty "File" <++> pretty f <++> pretty "written")
   displayResult (ProofFound x) = printResult (prettyTerm x)
   displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
@@ -1106,7 +1106,7 @@ mutual
   displayResult (RequestedHelp) = printResult (pretty displayHelp)
   displayResult (Edited (DisplayEdit Empty)) = pure ()
   displayResult (Edited (DisplayEdit xs)) = printResult xs
-  displayResult (Edited (EditError x)) = printError x
+  displayResult (Edited (EditError x)) = printResult x
   displayResult (Edited (MadeLemma lit name pty pappstr))
     = printResult $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
   displayResult (Edited (MadeWith lit wapp)) = printResult $ pretty $ showSep "\n" (map (relit lit) wapp)

src/Idris/REPL/Common.idr

@@ -48,9 +48,14 @@ iputStrLn msg
                                  toSExp !(renderWithoutColor msg), toSExp i])
 
 
-data MsgStatus = MsgStatusError | MsgStatusInfo
+||| Sampled against `VerbosityLvl`.
+public export
+data MsgStatus = MsgStatusNone | MsgStatusError | MsgStatusInfo
 
 doPrint : MsgStatus -> VerbosityLvl -> Bool
+doPrint MsgStatusNone  InfoLvl  = True
+doPrint MsgStatusNone  ErrorLvl = True
+doPrint MsgStatusNone  NoneLvl  = True
 doPrint MsgStatusError InfoLvl  = True
 doPrint MsgStatusError ErrorLvl = True
 doPrint MsgStatusError NoneLvl  = False
@@ -70,16 +75,21 @@ printWithStatus render msg status
              False  => pure ()
          IDEMode {} => pure () -- this function should never be called in IDE Mode
 
+||| Print REPL result.
 export
 printResult : {auto o : Ref ROpts REPLOpts} ->
               Doc IdrisAnn -> Core ()
-printResult x = printWithStatus render x MsgStatusInfo
+printResult x = printWithStatus render x MsgStatusNone
+ --                                      ^^^^^^^^^^^^^
+ -- "results" are printed no matter the verbosity level
 
+||| Print REPL result.
 export
 printDocResult : {auto o : Ref ROpts REPLOpts} ->
                  Doc IdrisDocAnn -> Core ()
-printDocResult x = printWithStatus (render styleAnn) x MsgStatusInfo
-
+printDocResult x = printWithStatus (render styleAnn) x MsgStatusNone
+ --                                                    ^^^^^^^^^^^^^
+ -- "results" are printed no matter the verbosity level
 
 -- Return that a protocol request failed somehow
 export