package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cDebug.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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type flag = bool ref

type t = (unit -> Pp.t) -> unit

let debug = ref CString.Map.empty

(* Used to remember level of Set Debug "all" for debugs created by
   plugins dynlinked after the Set *)
let all_flag = ref false

let set_debug_backtrace b =
  Exninfo.record_backtrace b

let set_debug_all b =
  set_debug_backtrace b;
  CString.Map.iter (fun _ flag -> flag := b) !debug;
  all_flag := b

let create_full ~name () =
  let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in
  let () = match name with
    | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.")
    | _ ->
      if CString.Map.mem name !debug then
        anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.")
  in
  let pp x =
    Feedback.msg_debug Pp.(hv 2 (str "[" ++ str name ++ str "]" ++ spc() ++ x))
  in
  let flag = ref !all_flag in
  debug := CString.Map.add name flag !debug;
  let pp x =
    if !flag
    then pp (x ())
  in
  flag, pp

let create ~name () =
  snd (create_full ~name ())

let get_flag flag = !flag

let set_flag flag v = flag := v

let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag"
    Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".")

let get_flags () =
  let pp_flag name flag = if flag then name else "-"^name in
  let flags =
    CString.Map.fold
      (fun name v acc -> pp_flag name !v :: acc)
      !debug []
  in
  let all = pp_flag "all" !all_flag in
  let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in
  String.concat "," (all::bt::flags)

exception Error

let parse_flags s =
  let parse_flag s =
    if CString.is_empty s then raise Error
    else if s.[0] = '-'
    then String.sub s 1 (String.length s - 1), false
    else s, true
  in
  try
    Some (CList.map parse_flag @@ String.split_on_char ',' s)
  with Error -> None

let set_flags s = match parse_flags s with
  | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.")
  | Some flags ->
    let set_one_flag (name,b) = match name with
      | "all" -> set_debug_all b
      | "backtrace" -> set_debug_backtrace b
      | _ -> match CString.Map.find_opt name !debug with
        | None -> warn_unknown_debug name
        | Some flag -> flag := b
    in
    List.iter set_one_flag flags

let misc, pp_misc = create_full ~name:"misc" ()
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct