[ fix ] auto-complete known log topics

src/Idris/SetOptions.idr

@@ -175,123 +175,8 @@ prefixOnlyIfNonEmpty s    = prefixOnly s
 codegens : {auto c : Ref Ctxt Defs} -> Core (List String)
 codegens = map fst . availableCGs . options <$> get Ctxt
 
--- list of log levels
--- currently generated manually
--- TODO: #1124
 logLevels : List String
-logLevels =
-  [ "auto"
-  , "builtin.Natural"
-  , "builtin.Natural.addTransform"
-  , "builtin.NaturalToInteger"
-  , "builtin.NaturalToInteger.addTransforms"
-  , "compile.casetree"
-  , "compiler.inline.eval"
-  , "compiler.refc"
-  , "compiler.refc.cc"
-  , "coverage"
-  , "coverage.empty"
-  , "coverage.missing"
-  , "coverage.recover"
-  , "declare.data"
-  , "declare.data.constructor"
-  , "declare.data.parameters"
-  , "declare.def"
-  , "declare.def.clause"
-  , "declare.def.clause.impossible"
-  , "declare.def.clause.with"
-  , "declare.def.impossible"
-  , "declare.def.lhs"
-  , "declare.def.lhs.implicits"
-  , "declare.param"
-  , "declare.record"
-  , "declare.record.field"
-  , "declare.record.projection"
-  , "declare.record.projection.prefix"
-  , "declare.type"
-  , "desugar.idiom"
-  , "doc.record"
-  , "elab"
-  , "elab.ambiguous"
-  , "elab.app.lhs"
-  , "elab.as"
-  , "elab.binder"
-  , "elab.bindnames"
-  , "elab.case"
-  , "elab.def.local"
-  , "elab.delay"
-  , "elab.hole"
-  , "elab.implementation"
-  , "elab.implicits"
-  , "elab.interface"
-  , "elab.interface.default"
-  , "elab.local"
-  , "elab.prun"
-  , "elab.prune"
-  , "elab.record"
-  , "elab.retry"
-  , "elab.rewrite"
-  , "elab.unify"
-  , "elab.update"
-  , "elab.with"
-  , "eval.casetree"
-  , "eval.casetree.stuck"
-  , "eval.eta"
-  , "eval.ref.bound"
-  , "eval.ref.data"
-  , "eval.ref.func"
-  , "eval.ref.type"
-  , "eval.stuck"
-  , "ide-mode.highlight"
-  , "ide-mode.highlight.alias"
-  , "ide-mode.highlighting.alias"
-  , "idemode.hole"
-  , "ide-mode.send"
-  , "import"
-  , "import.file"
-  , "interaction.casesplit"
-  , "interaction.generate"
-  , "interaction.search"
-  , "metadata.names"
-  , "quantity"
-  , "quantity.hole"
-  , "quantity.hole.update"
-  , "repl.eval"
-  , "totality"
-  , "totality.positivity"
-  , "totality.termination"
-  , "totality.termination.calc"
-  , "totality.termination.guarded"
-  , "totality.termination.sizechange"
-  , "totality.termination.sizechange.checkCall"
-  , "totality.termination.sizechange.checkCall.inPath"
-  , "totality.termination.sizechange.checkCall.inPathNot.restart"
-  , "totality.termination.sizechange.checkCall.inPathNot.return"
-  , "totality.termination.sizechange.inPath"
-  , "totality.termination.sizechange.isTerminating"
-  , "totality.termination.sizechange.needsChecking"
-  , "ttc.read"
-  , "ttc.write"
-  , "typesearch.equiv"
-  , "unelab.case"
-  , "unify"
-  , "unify.application"
-  , "unify.binder"
-  , "unify.constant"
-  , "unify.constraint"
-  , "unify.delay"
-  , "unify.equal"
-  , "unify.head"
-  , "unify.hole"
-  , "unify.instantiate"
-  , "unify.invertible"
-  , "unify.meta"
-  , "unify.noeta"
-  , "unify.postpone"
-  , "unify.retry"
-  , "unify.search"
-  , "unify.unsolved"
-  ]
+logLevels = map fst knownTopics
 
 -- given a pair of strings, the first representing the word
 -- actually being edited, the second representing the word