[ debug ] Give the option to log off

src/Core/Context.idr

@@ -2214,10 +2214,12 @@ getPrimitiveNames = pure $ catMaybes [!fromIntegerName, !fromStringName, !fromCh
 
 export
 addLogLevel : {auto c : Ref Ctxt Defs} ->
-              LogLevel -> Core ()
-addLogLevel l
+              Maybe LogLevel -> Core ()
+addLogLevel lvl
     = do defs <- get Ctxt
-         put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
+         case lvl of
+           Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs)
+           Just l  => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
 
 export
 withLogLevel : {auto c : Ref Ctxt Defs} ->

src/Idris/Desugar.idr

@@ -824,7 +824,7 @@ mutual
   desugarDecl ps (PDirective fc d)
       = case d of
              Hide n => pure [IPragma (\nest, env => hide fc n)]
-             Logging i => pure [ILog (topics i, verbosity i)]
+             Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
              LazyOn a => pure [IPragma (\nest, env => lazyActive a)]
              UnboundImplicits a => do
                setUnboundImplicits a

src/Idris/Parser.idr

@@ -951,6 +951,13 @@ totalityOpt
   <|> (keyword "total" *> pure Total)
   <|> (keyword "covering" *> pure CoveringOnly)
 
+logLevel : Rule (Maybe LogLevel)
+logLevel
+  = (Nothing <$ exactIdent "off")
+    <|> do topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
+           lvl <- intLit
+           pure (Just (mkLogLevel' topic (fromInteger lvl)))
+
 directive : FileName -> IndentInfo -> Rule Directive
 directive fname indents
     = do pragma "hide"
@@ -962,10 +969,9 @@ directive fname indents
 --          atEnd indents
 --          pure (Hide True n)
   <|> do pragma "logging"
-         topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
-         lvl <- intLit
+         lvl <- logLevel
          atEnd indents
-         pure (Logging (mkLogLevel' topic (fromInteger lvl)))
+         pure (Logging lvl)
   <|> do pragma "auto_lazy"
          b <- onoff
          atEnd indents
@@ -1401,9 +1407,9 @@ collectDefs [] = []
 collectDefs (PDef annot cs :: ds)
     = let (csWithFC, rest) = spanBy isPDef ds
           cs' = cs ++ concat (map snd csWithFC)
-          annot' = foldr 
+          annot' = foldr
                    (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
-                   annot 
+                   annot
                    (map fst csWithFC)
       in
           PDef annot' cs' :: assert_total (collectDefs rest)
@@ -1768,7 +1774,7 @@ compileArgsCmd parseCmd command doc
       tm <- expr pdef "(interactive)" init
       pure (command tm n)
 
-loggingArgCmd : ParseCmd -> (LogLevel -> REPLCmd) -> String -> CommandDefinition
+loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
 loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, parse) where
 
   names : List String
@@ -1778,9 +1784,8 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
   parse = do
     symbol ":"
     runParseCmd parseCmd
-    topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
-    lvl <- intLit
-    pure (command (mkLogLevel' topic (fromInteger lvl)))
+    lvl <- logLevel
+    pure (command lvl)
 
 parserCommandsForHelp : CommandTable
 parserCommandsForHelp =

src/Idris/REPL.idr

@@ -530,7 +530,7 @@ data REPLResult : Type where
   CheckedTotal : List (Name, Totality) -> REPLResult
   FoundHoles : List HoleData -> REPLResult
   OptionsSet : List REPLOpt -> REPLResult
-  LogLevelSet : LogLevel -> REPLResult
+  LogLevelSet : Maybe LogLevel -> REPLResult
   ConsoleWidthSet : Maybe Nat -> REPLResult
   ColorSet : Bool -> REPLResult
   VersionIs : Version -> REPLResult
@@ -965,7 +965,8 @@ mutual
   displayResult (FoundHoles xs) = do
     let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
     printResult (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
-  displayResult (LogLevelSet k) = printResult (reflow "Set loglevel to" <++> pretty k)
+  displayResult (LogLevelSet Nothing) = printResult (reflow "Logging turned off")
+  displayResult (LogLevelSet (Just k)) = printResult (reflow "Set log level to" <++> pretty k)
   displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)
   displayResult (ConsoleWidthSet Nothing) = printResult (reflow "Set consolewidth to auto")
   displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))

src/Idris/Syntax.idr

@@ -225,7 +225,7 @@ mutual
   public export
   data Directive : Type where
        Hide : Name -> Directive
-       Logging : LogLevel -> Directive
+       Logging : Maybe LogLevel -> Directive
        LazyOn : Bool -> Directive
        UnboundImplicits : Bool -> Directive
        AmbigDepth : Nat -> Directive
@@ -442,7 +442,7 @@ data REPLCmd : Type where
      Total : Name -> REPLCmd
      Doc : Name -> REPLCmd
      Browse : Namespace -> REPLCmd
-     SetLog : LogLevel -> REPLCmd
+     SetLog : Maybe LogLevel -> REPLCmd
      SetConsoleWidth : Maybe Nat -> REPLCmd
      SetColor : Bool -> REPLCmd
      Metavars : REPLCmd

src/TTImp/Parser.idr

@@ -647,14 +647,20 @@ namespaceDecl
          commit
          namespaceId
 
+logLevel : Rule (Maybe (List String, Nat))
+logLevel
+  = (Nothing <$ exactIdent "off")
+    <|> do topic <- option [] ((::) <$> unqualifiedName <*> many aDotIdent)
+           lvl <- intLit
+           pure (Just (topic, fromInteger lvl))
+
 directive : FileName -> IndentInfo -> Rule ImpDecl
 directive fname indents
     = do pragma "logging"
          commit
-         topic <- ((::) <$> unqualifiedName <*> many aDotIdent)
-         lvl <- intLit
+         lvl <- logLevel
          atEnd indents
-         pure (ILog (topic, integerToNat lvl))
+         pure (ILog lvl)
          {- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?
   <|> do pragma "pair"
          commit

src/TTImp/ProcessDecls.idr

@@ -59,7 +59,7 @@ process eopts nest env (IRunElabDecl fc tm)
 process eopts nest env (IPragma act)
     = act nest env
 process eopts nest env (ILog lvl)
-    = addLogLevel (uncurry unsafeMkLogLevel lvl)
+    = addLogLevel (uncurry unsafeMkLogLevel <$> lvl)
 
 TTImp.Elab.Check.processDecl = process
 

src/TTImp/TTImp.idr

@@ -347,7 +347,7 @@ mutual
        IPragma : ({vars : _} ->
                   NestedNames vars -> Env Term vars -> Core ()) ->
                  ImpDecl
-       ILog : (List String, Nat) -> ImpDecl
+       ILog : Maybe (List String, Nat) -> ImpDecl
 
   export
   Show ImpDecl where
@@ -366,7 +366,8 @@ mutual
     show (IRunElabDecl _ tm)
         = "%runElab " ++ show tm
     show (IPragma _) = "[externally defined pragma]"
-    show (ILog (topic, lvl)) = "%logging " ++ case topic of
+    show (ILog Nothing) = "%logging off"
+    show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
       [] => show lvl
       _  => concat (intersperse "." topic) ++ " " ++ show lvl
 

tests/idris2/positivity002/Issue660.idr

@@ -9,3 +9,7 @@ data C : Type -> Type where
 
 data D : Type -> Type where
   MkD : {0 a : Type} -> let 0 b = List a in b -> D a
+
+%logging off
+
+data E : Type where