package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/src/lambdapi.common/logger.ml.html
Source file logger.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
(** Functions for creating loggers. **) open Lplib open Base open Color (** Type of a logging function. It needs to be boxed for higher-rank polymorphism reasons *) type logger_pp = { pp: 'a. 'a outfmt -> 'a } (** Type of logging function data. *) type logger = { logger_key : char (** Character used to unable the logger. *) ; logger_name : string (** Four-characters name used as prefix in logs. *) ; logger_desc : string (** Description of the log displayed in help. *) ; logger_enabled : bool ref (** Is the log enabled? *) ; logger_pp : logger_pp (** Type of a logging function. *) } let cmp l1 l2 = Stdlib.compare l1.logger_key l2.logger_key (** [loggers] contains the registered logging functions. *) let loggers : logger list Stdlib.ref = Stdlib.ref [] let add_logger l = Stdlib.(loggers := Lplib.List.insert cmp l !loggers) (** [log_enabled] is the cached result of whether there exists an enabled logging function. Its main use is to guard logging operations to avoid performing unnecessary computations.*) let _log_enabled = ref false let log_enabled () = !_log_enabled let update_log_enabled () = _log_enabled := List.exists (fun logger -> !(logger.logger_enabled)) Stdlib.(!loggers) (** [make key name desc] registers a new logger and returns its pp. *) let make logger_key logger_name logger_desc = (* Sanity checks. *) if String.length logger_name <> 4 then invalid_arg "Logger.make: name must be 4 characters long"; let check data = if logger_key = data.logger_key then invalid_arg "Logger.make: key is already used"; if logger_name = data.logger_name then invalid_arg "Logger.make: name is already used" in List.iter check Stdlib.(!loggers); let logger_enabled = ref false in (* Actual printing function. *) let pp fmt = update_with_color Stdlib.(!Error.err_fmt); let out = Format.(if !logger_enabled then fprintf else ifprintf) in out Stdlib.(!Error.err_fmt) (cya "[%s]" ^^ " @[" ^^ fmt ^^ "@]@.") logger_name in (* Logger registration. *) let logger = { logger_key ; logger_name ; logger_desc ; logger_enabled ; logger_pp = { pp } } in add_logger logger; logger.logger_pp (** [set_debug value key] enables or disables the loggers corresponding to every character of [str] according to [value]. *) let set_debug value str = let fn { logger_key; logger_enabled; _ } = if String.contains str logger_key then logger_enabled := value in List.iter fn Stdlib.(!loggers); update_log_enabled () (** [default_loggers] lists the loggers enabled by default, in a string. *) let default_loggers = Stdlib.ref "" (** [set_default_debug str] declares the debug flags of [str] to be enabled by default. *) let set_default_debug str = Stdlib.(default_loggers := str); set_debug true str (** [get_activated_loggers ()] fetches the list of activated loggers, listed in a string *) let get_activated_loggers () = Stdlib.(!loggers) |> List.filter_map (fun logger -> if !(logger.logger_enabled) then Some (String.make 1 logger.logger_key) else None) |> String.concat "" (** [reset_loggers ~default ()] resets the debug flags to those in default. Without the optional argument, use [!default_loggers] *) let reset_loggers ?(default=Stdlib.(! default_loggers)) () = let default_value = String.contains default in let fn { logger_key; logger_enabled; _ } = logger_enabled := default_value logger_key in List.iter fn Stdlib.(!loggers); update_log_enabled () (** [log_summary ()] gives the keys and descriptions for logging options. *) let log_summary () = List.map (fun d -> (d.logger_key, d.logger_desc)) Stdlib.(!loggers)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>