From 3d33b59d725760bee14668c744b057a75440012e Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Tue, 23 Jun 2015 14:49:01 +0200 Subject: Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. This allows fatal_error to be used for printing anomalies at loading time. --- printing/ppstyle.ml | 149 ------------------------------------------------ printing/ppstyle.mli | 70 ----------------------- printing/printing.mllib | 1 - 3 files changed, 220 deletions(-) delete mode 100644 printing/ppstyle.ml delete mode 100644 printing/ppstyle.mli (limited to 'printing') diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml deleted file mode 100644 index fb334c706..000000000 --- a/printing/ppstyle.ml +++ /dev/null @@ -1,149 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 - () diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli deleted file mode 100644 index f5d6184cb..000000000 --- a/printing/ppstyle.mli +++ /dev/null @@ -1,70 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list -> t -(** Create a new tag with the given name. Each name must be unique. The optional - style is taken as the default one. *) - -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! *) - -val pp_tag : Pp.tag_handler -(** Returns the name of a style tag that is understandable by the formatters - that have been inititialized through {!init_color_output}. To be used with - {!Pp.pp_with}. *) - -(** {5 Tags} *) - -val error_tag : t -(** Tag used by the {!Pp.msg_error} function. *) - -val warning_tag : t -(** Tag used by the {!Pp.msg_warning} function. *) - -val debug_tag : t -(** Tag used by the {!Pp.msg_debug} function. *) diff --git a/printing/printing.mllib b/printing/printing.mllib index 7b4c71a8b..652a34fa1 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,5 @@ Genprint Pputils -Ppstyle Ppannotation Ppconstr Ppconstrsig -- cgit v1.2.3