diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index e14f95b08..7d3a5171f 100644 --- a/src/Idris/SetOptions.idr +++ b/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