From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- lib/pp.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..01df2510cf 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -412,7 +412,7 @@ type message_level = Feedback.message_level = type message = Feedback.message = { message_level : message_level; - message_content : string; + message_content : Xml_datatype.xml; } let of_message = Feedback.of_message @@ -511,11 +511,11 @@ let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () -let log_via_feedback () = logger := (fun ~id lvl msg -> +let log_via_feedback printer = logger := (fun ~id lvl msg -> !feeder { Feedback.contents = Feedback.Message { message_level = lvl; - message_content = string_of_ppcmds msg }; + message_content = printer msg }; Feedback.route = !feedback_route; Feedback.id = id }) -- cgit v1.2.3 From 832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 2 Oct 2015 14:41:29 +0200 Subject: emacs output mode: Added tag to debug messages. So that they display in response buffer. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..1711008ead 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -424,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit let make_body info s = emacs_quote (hov 0 (info ++ spc () ++ s)) -let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) +let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) let warnbody strm = make_body (str "Warning:") strm let errorbody strm = make_body (str "Error:") strm let infobody strm = emacs_quote_info strm -- cgit v1.2.3 From de32427bd2785c365374c554b4b74e97749cb995 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 11:28:30 +0200 Subject: Fixed #4274, bad formatting of messages in emacs mode. --- lib/pp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 1711008ead..4ed4b17791 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -362,11 +362,11 @@ let emacs_quote_info_start = "" let emacs_quote_info_end = "" let emacs_quote g = - if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end + if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) else hov 0 g let emacs_quote_info g = - if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end + if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) else hov 0 g -- cgit v1.2.3 From 126a3c998c62bfd9f9b570f12b2e29576dd94cdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 13:43:07 +0100 Subject: Factorizing unsafe code by relying on the new Dyn module. --- lib/pp.ml | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 146d3562dd..a1913c98f7 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -51,25 +51,18 @@ sig val prj : t -> 'a key -> 'a option end = struct - (** See module {Dyn} for more details. *) - type t = int * Obj.t - - type 'a key = int - - let dyntab = ref (Int.Map.empty : string Int.Map.t) - - let create (s : string) = - let hash = Hashtbl.hash s in - let () = assert (not (Int.Map.mem hash !dyntab)) in - let () = dyntab := Int.Map.add hash s !dyntab in - hash - - let inj x h = (h, Obj.repr x) - - let prj (nh, rv) h = - if Int.equal h nh then Some (Obj.magic rv) - else None +module Dyn = Dyn.Make(struct end) + +type t = Dyn.t +type 'a key = 'a Dyn.tag +let create = Dyn.create +let inj x k = Dyn.Dyn (k, x) +let prj : type a. t -> a key -> a option = fun dyn k -> + let Dyn.Dyn (k', x) = dyn in + match Dyn.eq k k' with + | None -> None + | Some CSig.Refl -> Some x end -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 4ed4b17791..4f50e3e19b 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* s,None in - com_if ft (Lazy.lazy_from_val()); + com_if ft (Lazy.from_val()); (* let s1 = if String.length s1 <> 0 && s1.[0] = ' ' then (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1)) @@ -290,29 +290,29 @@ let pp_dirs ?pp_tag ft = begin match tok with | Str_def s -> let n = utf8_length s in - com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s + com_if ft (Lazy.from_val()); Format.pp_print_as ft n s | Str_len (s, n) -> - com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s + com_if ft (Lazy.from_val()); Format.pp_print_as ft n s end | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - com_if ft (Lazy.lazy_from_val()); + com_if ft (Lazy.from_val()); pp_open_box bty ; if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty + | Ppcmd_open_box bty -> com_if ft (Lazy.from_val()); pp_open_box bty | Ppcmd_close_box -> Format.pp_close_box ft () | Ppcmd_close_tbox -> Format.pp_close_tbox ft () | Ppcmd_white_space n -> - com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0)) + com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0)) | Ppcmd_print_break(m,n) -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n)) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n)) | Ppcmd_set_tab -> Format.pp_set_tab ft () | Ppcmd_print_tbreak(m,n) -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n)) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n)) | Ppcmd_force_newline -> com_brk ft; Format.pp_force_newline ft () | Ppcmd_print_if_broken -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ())) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ())) | Ppcmd_comment i -> let coms = split_com [] [] i !comments in (* Format.pp_open_hvbox ft 0;*) -- cgit v1.2.3 From ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 11:56:53 +0200 Subject: In pr_clauses, do not print a leading space by default so that it can be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. --- lib/pp.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 9a833ae225..c7cf9b8d0e 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -518,6 +518,7 @@ let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x +let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x -- cgit v1.2.3