diff options
-rw-r--r-- | lib/cErrors.ml | 4 | ||||
-rw-r--r-- | lib/feedback.ml | 10 | ||||
-rw-r--r-- | lib/pp.ml | 24 | ||||
-rw-r--r-- | lib/pp.mli | 26 | ||||
-rw-r--r-- | lib/ppstyle.ml | 36 | ||||
-rw-r--r-- | lib/ppstyle.mli | 20 | ||||
-rw-r--r-- | lib/richpp.ml | 5 | ||||
-rw-r--r-- | lib/richpp.mli | 2 | ||||
-rw-r--r-- | parsing/cLexer.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
-rw-r--r-- | printing/ppconstr.ml | 2 | ||||
-rw-r--r-- | printing/printmod.ml | 40 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 4 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 | ||||
-rw-r--r-- | vernac/explainErr.ml | 2 |
15 files changed, 67 insertions, 114 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index dbebe6a48..9cbc3fb6d 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -22,7 +22,7 @@ exception Anomaly of string option * std_ppcmds (* System errors *) * Anyways, tagging should not happen here, but in the specific * listener to the msg_* stuff. *) -let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc () +let tag_err_str s = tag Ppstyle.error_tag (str s) ++ spc () let err_str = tag_err_str "Error:" let ann_str = tag_err_str "Anomaly:" @@ -154,6 +154,6 @@ let handled e = let fatal_error info anomaly = let msg = info ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; + pp_with !Pp_control.err_ft msg; Format.pp_print_flush !Pp_control.err_ft (); exit (if anomaly then 129 else 1) diff --git a/lib/feedback.ml b/lib/feedback.ml index 57c6f30a4..e723bf4ba 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -73,10 +73,10 @@ end open Emacs -let dbg_str = tag Ppstyle.(Tag.inj debug_tag tag) (str "Debug:") ++ spc () +let dbg_str = tag Ppstyle.debug_tag (str "Debug:") ++ spc () let info_str = mt () -let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc () -let err_str = tag Ppstyle.(Tag.inj error_tag tag) (str "Error:" ) ++ spc () +let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc () +let err_str = tag Ppstyle.error_tag (str "Error:" ) ++ spc () let make_body quoter info ?loc s = let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in @@ -132,7 +132,7 @@ let make_style_stack () = | st :: _ -> st in let push tag = - let style = match Ppstyle.get_style tag with + let style = match Ppstyle.get_style_format tag with | None -> empty | Some st -> st in @@ -156,7 +156,7 @@ let init_color_output () = let open Pp_control in let push_tag, pop_tag, clear_tag = make_style_stack () in std_logger_cleanup := clear_tag; - std_logger_tag := Some Ppstyle.pp_tag; + std_logger_tag := Some Ppstyle.to_format; let tag_handler = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; @@ -42,25 +42,7 @@ end = struct end -module Tag : -sig - type t - type 'a key - val create : string -> 'a key - val inj : 'a -> 'a key -> t - val prj : t -> 'a key -> 'a option -end = -struct - -module Dyn = Dyn.Make(struct end) - -type t = Dyn.t -type 'a key = 'a Dyn.tag -let create = Dyn.create -let inj = Dyn.Easy.inj -let prj = Dyn.Easy.prj - -end +type pp_tag = string list open Pp_control @@ -95,7 +77,7 @@ type 'a ppcmd_token = | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_open_tag of Tag.t + | Ppcmd_open_tag of pp_tag | Ppcmd_close_tag type 'a ppdir_token = @@ -243,7 +225,7 @@ let rec pr_com ft s = Some s2 -> Format.pp_force_newline ft (); pr_com ft s2 | None -> () -type tag_handler = Tag.t -> Format.tag +type tag_handler = pp_tag -> Format.tag (* pretty printing functions *) let pp_dirs ?pp_tag ft = diff --git a/lib/pp.mli b/lib/pp.mli index f17908262..64ebea196 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -67,27 +67,11 @@ val close : unit -> std_ppcmds (** {6 Opening and closing of tags} *) -module Tag : -sig - type t - (** Type of tags. Tags are dynamic types comparable to {Dyn.t}. *) +(* XXX: Improve and add attributes *) +type pp_tag = string list - type 'a key - (** Keys used to inject tags *) - - val create : string -> 'a key - (** Create a key with the given name. Two keys cannot share the same name, if - ever this is the case this function raises an assertion failure. *) - - val inj : 'a -> 'a key -> t - (** Inject an object into a tag. *) - - val prj : t -> 'a key -> 'a option - (** Project an object from a tag. *) -end - -val tag : Tag.t -> std_ppcmds -> std_ppcmds -val open_tag : Tag.t -> std_ppcmds +val tag : pp_tag -> std_ppcmds -> std_ppcmds +val open_tag : pp_tag -> std_ppcmds val close_tag : unit -> std_ppcmds (** {6 Utilities} *) @@ -165,7 +149,7 @@ val pr_loc : Loc.t -> std_ppcmds (** {6 Low-level pretty-printing functions with and without flush} *) (** FIXME: These ignore the logging settings and call [Format] directly *) -type tag_handler = Tag.t -> Format.tag +type tag_handler = pp_tag -> Format.tag (** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt] *) val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index aa47c5167..298e3be6b 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -8,32 +8,38 @@ module String = CString -type t = string -(** We use the concatenated string, with dots separating each string. We - forbid the use of dots in the strings. *) +type t = Pp.pp_tag let tags : Terminal.style option String.Map.t ref = ref String.Map.empty +let to_format tag = String.concat "." tag +let of_format tag = String.split '.' tag + 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 name = to_format tag in let () = assert (not (String.Map.mem name !tags)) in - let () = tags := String.Map.add name style !tags in - name + let () = tags := String.Map.add name style !tags in + tag -let repr t = String.split '.' t +let repr t = t let get_style tag = - try String.Map.find tag !tags with Not_found -> assert false + try String.Map.find (to_format tag) !tags + with Not_found -> assert false + +let get_style_format 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 + try tags := String.Map.update (to_format 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 dump () = + List.map (fun (s,b) -> (String.split '.' s, b)) (String.Map.bindings !tags) let parse_config s = let styles = Terminal.parse s in @@ -42,8 +48,6 @@ let parse_config s = 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; @@ -67,7 +71,3 @@ let warning_tag = 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 diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index d9fd75765..b9422f7cf 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -11,7 +11,11 @@ (** {5 Style tags} *) -type t = string +(** This API is provisional and will likely be refined. *) +type t = Pp.pp_tag + +val to_format : t -> Format.tag +val of_format : Format.tag -> t (** Style tags *) @@ -23,14 +27,15 @@ 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 get_style_format : Format.tag -> Terminal.style option +(** Get the style associated to a tag from a format tag. *) + + val set_style : t -> Terminal.style option -> unit (** Set a style associated to a tag. *) @@ -44,13 +49,6 @@ val parse_config : string -> unit val dump : unit -> (t * Terminal.style option) list (** Recover the list of known tags together with their current style. *) -(** {5 Color output} *) - -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 diff --git a/lib/richpp.ml b/lib/richpp.ml index d1c6d158e..c0128dbc2 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -177,10 +177,7 @@ let richpp_of_xml xml = xml let richpp_of_string s = PCData s let richpp_of_pp pp = - let annotate t = match Pp.Tag.prj t Ppstyle.tag with - | None -> None - | Some key -> Some (Ppstyle.repr key) - in + let annotate t = Some (Ppstyle.repr t) in let rec drop = function | PCData s -> [PCData s] | Element (_, annotation, cs) -> diff --git a/lib/richpp.mli b/lib/richpp.mli index 287d265a8..2e839e996 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -22,7 +22,7 @@ type 'annotation located = { The [get_annotations] function is used to convert tags into the desired annotation. *) val rich_pp : - (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> + (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> 'annotation located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 72bd11e03..a637d2e43 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -105,7 +105,7 @@ module Error = struct Printf.sprintf "Unsupported Unicode character (0x%x)" x) (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x)) + let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.to_format ppf (Pp.str (to_string x)) end open Error diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 9dacce28d..d9410a088 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -43,7 +43,7 @@ struct end -let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s +let tag t s = Pp.tag t s let do_not_tag _ x = x let tag_keyword = tag Tag.keyword let tag_primitive = tag Tag.primitive diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b16384c60..c772f7be1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -52,7 +52,7 @@ struct end let do_not_tag _ x = x -let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s +let tag t s = Pp.tag t s let tag_keyword = tag Tag.keyword let tag_evar = tag Tag.evar let tag_type = tag Tag.univ diff --git a/printing/printmod.ml b/printing/printmod.ml index dfa66d437..ac7ff7697 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -26,6 +26,20 @@ open Goptions the "short" mode or (Some env) in the "rich" one. *) +module Tag = +struct + let definition = + let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in + Ppstyle.make ~style ["module"; "definition"] + let keyword = + let style = Terminal.make ~bold:true () in + Ppstyle.make ~style ["module"; "keyword"] +end + +let tag t s = Pp.tag t s +let tag_definition s = tag Tag.definition s +let tag_keyword s = tag Tag.keyword s + let short = ref false let _ = @@ -44,14 +58,8 @@ let mk_fake_top = let r = ref 0 in fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r)) -module Make (Taggers : sig - val tag_definition : std_ppcmds -> std_ppcmds - val tag_keyword : std_ppcmds -> std_ppcmds -end) = -struct - -let def s = Taggers.tag_definition (str s) -let keyword s = Taggers.tag_keyword (str s) +let def s = tag_definition (str s) +let keyword s = tag_keyword (str s) let get_new_id locals id = let rec get_id l id = @@ -441,20 +449,4 @@ let print_modtype kn = with e when CErrors.noncritical e -> print_signature' true None kn mtb.mod_type)) -end - -module Tag = -struct - let definition = - let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in - Ppstyle.make ~style ["module"; "definition"] - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["module"; "keyword"] -end -include Make(struct - let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s - let tag_definition s = tag Tag.definition s - let tag_keyword s = tag Tag.keyword s -end) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0dfd06726..5521e8a40 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -13,7 +13,7 @@ open Flags open Vernac open Pcoq -let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x +let top_stderr x = msg_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -309,7 +309,7 @@ let do_vernac () = | any -> let any = CErrors.push any in let msg = print_toplevel_error any ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; + pp_with !Pp_control.std_ft msg; Format.pp_print_flush !Pp_control.std_ft () (** Main coq loop : read vernacular expressions until Drop is entered. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b73321c00..de7bc6929 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -179,7 +179,7 @@ let pp_cmd_header loc com = and take control of the console. *) let print_cmd_header loc com = - Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com); + Pp.pp_with ~pp_tag:Ppstyle.to_format !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () let rec interp_vernac po chan_beautify checknav (loc,com) = diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 17897460c..148d029bc 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -47,7 +47,7 @@ let _ = CErrors.register_handler explain_exn_default let wrap_vernac_error with_header (exn, info) strm = if with_header then - let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in + let header = Pp.tag Ppstyle.error_tag (str "Error:") in let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in (e, info) else |