Adding a pretty-printing style library.

4 files changed, 187 insertions, 0 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 336a680bd..2e61cb697 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Terminal
 Hook
 Canary
 Hashset
@@ -153,6 +154,7 @@ Tok
 Lexer
 Ppextend
 Pputils
+Ppstyle
 Ppannotation
 Stdarg
 Constrarg
diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml
new file mode 100644
index 000000000..84fe99ca3
--- /dev/null
+++ b/printing/ppstyle.ml
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \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 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 None !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 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 pp_tag t = match Pp.Tag.prj t tag with
+  | None -> ""
+  | Some key -> key
+  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 open Pp in
+  let msg ?header ft strm =
+    let strm = match header with
+    | None -> hov 0 strm
+    | Some h -> hov 0 (str h ++ str ":" ++ 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" !std_ft strm
+  | Info -> msg !std_ft strm
+  | Notice -> msg !std_ft strm
+  | Warning -> Flags.if_warn (fun () -> msg ~header:"Warning" !err_ft strm) ()
+  | Error -> msg ~header:"Error" !err_ft strm
+  in
+  let () = set_logger logger in
+  ()
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli
new file mode 100644
index 000000000..5fd9e074d
--- /dev/null
+++ b/printing/ppstyle.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Highlighting of printers. Used for pretty-printing terms that should be
+    displayed on a color-capable terminal. *)
+
+(** {5 Style tags} *)
+
+type t
+(** Style tags *)
+
+val make : string list -> t
+(** Create a new tag with the given name. Each name must be unique. *)
+
+val repr : t -> string list
+(** Gives back the original name of the style tag where each string has been
+    concatenated and separated with a dot. *)
+
+val tag : t Pp.Tag.key
+(** An annotation for styles *)
+
+(** {5 Manipulating global styles} *)
+
+val get_style : t -> Terminal.style option
+(** Get the style associated to a tag. *)
+
+val set_style : t -> Terminal.style option -> unit
+(** Set a style associated to a tag. *)
+
+val clear_styles : unit -> unit
+(** Clear all styles. *)
+
+val parse_config : string -> unit
+(** Add all styles from the given string as parsed by {!Terminal.parse}.
+    Unregistered tags are ignored. *)
+
+val dump : unit -> (t * Terminal.style option) list
+(** Recover the list of known tags together with their current style. *)
+
+(** {5 Setting color output} *)
+
+val init_color_output : unit -> unit
+(** Once called, all tags defined here will use their current style when
+    printed. To this end, this function redefines the loggers used when sending
+    messages to the user. The program will in particular use the formatters
+    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
+    with additional syle information provided by this module. Be careful this is
+    not compatible with the Emacs mode! *)
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 652a34fa1..7b4c71a8b 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,5 +1,6 @@
 Genprint
 Pputils
+Ppstyle
 Ppannotation
 Ppconstr
 Ppconstrsig