@@ -45,8 +45,27 @@ Use of this option will still result in the generation of the Idris binary ``.ib
4545Logging Output
4646==============
4747
48−Logging of the Idris output can be used to diagnose problems with the compilation of your program.
49−Idris supports the logging at various different levels of verbosity: 1 to 10.
48+The internal operation of Idris is captured using a category based logger.
49+Currently, the logging infrastructure has support for the following categories:
50+
51++ Parser
52++ Elaborator
53++ Code generation
54++ Erasure
55++ Coverage Checking
56++ IBC generation
57+
58+
59+These categories are specified using the command-line option:
60+``--logging-categories CATS``, where ``CATS`` is a quoted colon
61+seperated string of the categories you want to see. By default if this
62+option is not specified all categories are allowed. Sub-categories
63+have yet to be defined but will be in the future, especially for the
64+elaborator.
65+
66+Further, the verbosity of logging can be controlled by specifying a
67+logging level between: 1 to 10 using the command-line option: ``--log
68+<level>``.
5069
5170+ Level 0: Show no logging output. Default level
5271+ Level 1: High level details of the compilation process.