From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- ide/coqOps.ml | 4 ++-- ide/document.mli | 2 +- ide/ideutils.ml | 2 +- ide/ideutils.mli | 2 +- ide/interface.mli | 8 ++++---- ide/minilib.mli | 2 +- ide/richpp.mli | 4 ++-- ide/wg_MessageView.ml | 4 ++-- ide/wg_MessageView.mli | 4 ++-- ide/xmlprotocol.ml | 4 ++-- 10 files changed, 18 insertions(+), 18 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 3eb5b0753..364fc883b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -58,7 +58,7 @@ module SentenceId : sig val connect : sentence -> signals val dbg_to_string : - GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds + GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t end = struct @@ -163,7 +163,7 @@ let flags_to_color f = else `NAME Preferences.processed_color#get (* Move to utils? *) -let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with +let rec validate (s : Pp.t) = match Pp.repr s with | Pp.Ppcmd_empty | Pp.Ppcmd_print_break _ | Pp.Ppcmd_force_newline -> true diff --git a/ide/document.mli b/ide/document.mli index fb96cb6d7..ab8e71808 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -102,7 +102,7 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list (** debug print *) val print : - 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds + 'a document -> (bool -> id option -> 'a -> Pp.t) -> Pp.t (** Callbacks on documents *) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 2573b6d6f..83e5da950 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -316,7 +316,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit let default_logger level message = let level = match level with diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 458b8e0a5..f06a48aeb 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -67,7 +67,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/interface.mli b/ide/interface.mli index aab1d8272..1939a8427 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -17,9 +17,9 @@ type verbose = bool type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : Pp.std_ppcmds list; + goal_hyp : Pp.t list; (** List of hypotheses *) - goal_ccl : Pp.std_ppcmds; + goal_ccl : Pp.t; (** Goal conclusion *) } @@ -121,7 +121,7 @@ type edit_id = int should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * Pp.std_ppcmds) + | Fail of (state_id * location * Pp.t) type ('a, 'b) union = ('a, 'b) Util.union @@ -213,7 +213,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * Pp.std_ppcmds +type handle_exn_rty = state_id * location * Pp.t (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/minilib.mli b/ide/minilib.mli index 4517a2374..c96e59b22 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,7 @@ type level = [ (** debug printing *) val debug : bool ref -val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log_pp : ?level:level -> Pp.t -> unit val log : ?level:level -> string -> unit val coqide_config_home : unit -> string diff --git a/ide/richpp.mli b/ide/richpp.mli index f2ba15d22..84adc61ca 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,7 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml +val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -47,5 +47,5 @@ type richpp = Xml_datatype.xml (** Type of text with style annotations *) -val richpp_of_pp : int -> Pp.std_ppcmds -> richpp +val richpp_of_pp : int -> Pp.t -> richpp (** Extract style information from formatted text *) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index d2a09dd94..65df2b849 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,9 +28,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 0ce257c3d..6bd0625f0 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,9 +18,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 06c695c77..4b521a968 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -117,7 +117,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with +let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -149,7 +149,7 @@ let rec to_pp xpp = let open Pp in let of_richpp x = Element ("richpp", [], [x]) (* Run-time Selectable *) -let of_pp (pp : Pp.std_ppcmds) = +let of_pp (pp : Pp.t) = match !msg_format with | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) | Ppcmds -> of_pp pp -- cgit v1.2.3