summaryrefslogtreecommitdiff
path: root/printing/ppstyle.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppstyle.ml')
-rw-r--r--printing/ppstyle.ml149
1 files changed, 149 insertions, 0 deletions
diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml
new file mode 100644
index 00000000..fb334c70
--- /dev/null
+++ b/printing/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
+ ()