This formalisation is now part of the AFP. Please refer to https://www.isa-afp.org/entries/ML_Unification.html
A hierarchical logger for Isabelle/ML.
See ML_Logger_Examples.thy
for a quick overview.
Features:
- Per logger configuration, including, among other things,
- output function (e.g. print to console or file)
- log level: suppress and enable log messages based on severity
- message filter: suppress and enable log messages based on a filter function
- Hierarchical configuration: set options based on logger name spaces;
for example, disable logging for all loggers registered below
Root.Unification.*
- Logging antiquotation to optionally print positional information of logging message
- Commands and attributes to setup and configure loggers with ML code.