diff options
author | 2015-06-23 14:49:01 +0200 | |
---|---|---|
committer | 2015-06-23 18:21:33 +0200 | |
commit | 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (patch) | |
tree | ec32a18ad10f2afcfbe34801873ac7d74c6f2257 /lib/ppstyle.ml | |
parent | 19fed6f504eb8450dee34faa8e84a6d4071131dc (diff) |
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
This allows fatal_error to be used for printing anomalies at loading time.
Diffstat (limited to 'lib/ppstyle.ml')
-rw-r--r-- | lib/ppstyle.ml | 149 |
1 files changed, 149 insertions, 0 deletions
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml new file mode 100644 index 000000000..fb334c706 --- /dev/null +++ b/lib/ppstyle.ml @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util + +type t = string +(** We use the concatenated string, with dots separating each string. We + forbid the use of dots in the strings. *) + +let tags : Terminal.style option String.Map.t ref = ref String.Map.empty + +let make ?style tag = + let check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in + let () = List.iter check tag in + let name = String.concat "." tag in + let () = assert (not (String.Map.mem name !tags)) in + let () = tags := String.Map.add name style !tags in + name + +let repr t = String.split '.' t + +let get_style tag = + try String.Map.find tag !tags with Not_found -> assert false + +let set_style tag st = + try tags := String.Map.update tag st !tags with Not_found -> assert false + +let clear_styles () = + tags := String.Map.map (fun _ -> None) !tags + +let dump () = String.Map.bindings !tags + +let parse_config s = + let styles = Terminal.parse s in + let set accu (name, st) = + try String.Map.update name (Some st) accu with Not_found -> accu + in + tags := List.fold_left set !tags styles + +let tag = Pp.Tag.create "ppstyle" + +(** Default tag is to reset everything *) +let default = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; +}) + +let empty = Terminal.make () + +let make_style_stack style_tags = + (** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = + try + begin match String.Map.find tag style_tags with + | None -> empty + | Some st -> st + end + with Not_found -> empty + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + let () = style_stack := style :: !style_stack in + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> + (** Something went wrong, we fallback *) + Terminal.eval default + | _ :: rem -> + let () = style_stack := rem in + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let error_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in + make ~style ["message"; "error"] + +let warning_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in + make ~style ["message"; "warning"] + +let debug_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in + make ~style ["message"; "debug"] + +let pp_tag t = match Pp.Tag.prj t tag with +| None -> "" +| Some key -> key + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack !tags in + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } in + let open Pp_control in + let () = Format.pp_set_mark_tags !std_ft true in + let () = Format.pp_set_mark_tags !err_ft true in + let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in + let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in + let pptag = tag in + let open Pp in + let msg ?header ft strm = + let strm = match header with + | None -> hov 0 strm + | Some (h, t) -> + let tag = Pp.Tag.inj t pptag in + let h = Pp.tag tag (str h ++ str ":") in + hov 0 (h ++ spc () ++ strm) + in + pp_with ~pp_tag ft strm; + Format.pp_print_newline ft (); + Format.pp_print_flush ft (); + (** In case something went wrong, we reset the stack *) + clear_tag (); + in + let logger level strm = match level with + | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", error_tag) !err_ft strm + in + let () = set_logger logger in + () |