diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 14 | ||||
| -rw-r--r-- | lib/clib.mllib | 4 | ||||
| -rw-r--r-- | lib/feedback.ml | 177 | ||||
| -rw-r--r-- | lib/feedback.mli | 33 | ||||
| -rw-r--r-- | lib/pp.ml | 9 | ||||
| -rw-r--r-- | lib/pp.mli | 24 | ||||
| -rw-r--r-- | lib/pp_control.ml | 93 | ||||
| -rw-r--r-- | lib/pp_control.mli | 38 | ||||
| -rw-r--r-- | lib/richpp.ml | 200 | ||||
| -rw-r--r-- | lib/richpp.mli | 64 |
10 files changed, 43 insertions, 613 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index a059640394..99b763602d 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -16,16 +16,6 @@ let push = Backtrace.add_backtrace exception Anomaly of string option * std_ppcmds (* System errors *) -(* XXX: To move to common tagging functions in Pp, blocked on tag - * system cleanup as we cannot define generic error tags now. - * - * Anyways, tagging should not happen here, but in the specific - * listener to the msg_* stuff. - *) -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:" - let _ = let pr = function | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"") @@ -102,7 +92,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (ann_str ++ raw_anomaly e ++ spc () ++ + hov 0 (raw_anomaly e ++ spc () ++ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else @@ -124,7 +114,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (err_str ++ where s ++ pps) + hov 0 (where s ++ pps) | _ -> raise Unhandled end diff --git a/lib/clib.mllib b/lib/clib.mllib index 1e33173ee1..5a5f6afd39 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -15,7 +15,6 @@ Store Exninfo Backtrace IStream -Pp_control Flags Control Loc @@ -28,9 +27,8 @@ CStack Util Stateid Pp -Ppstyle -Richpp Feedback +Ppstyle CUnix Envars Aux_file diff --git a/lib/feedback.ml b/lib/feedback.ml index 852eec2f26..31677ecfc9 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -35,7 +35,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Generic messages *) - | Message of level * Loc.t option * Richpp.richpp + | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { id : edit_or_state_id; @@ -45,140 +45,6 @@ type feedback = { let default_route = 0 -(** Feedback and logging *) -open Pp -open Pp_control - -type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit - -let msgnl_with ?pp_tag fmt strm = - pp_with ?pp_tag fmt (strm ++ fnl ()); - Format.pp_print_flush fmt () - -(* XXX: This is really painful! *) -module Emacs = struct - - (* Special chars for emacs, to detect warnings inside goal output *) - let emacs_quote_start = String.make 1 (Char.chr 254) - let emacs_quote_end = String.make 1 (Char.chr 255) - - let emacs_quote_err g = - hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) - - let emacs_quote_info_start = "<infomsg>" - let emacs_quote_info_end = "</infomsg>" - - let emacs_quote_info g = - hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) - -end - -open Emacs - -let dbg_str = tag Ppstyle.debug_tag (str "Debug:") ++ spc () -let info_str = mt () -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 - quoter (hov 0 (loc ++ info ++ s)) - -(* Generic logger *) -let gen_logger dbg err ?pp_tag ?loc level msg = match level with - | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) - | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) - | Notice -> msgnl_with ?pp_tag !std_ft msg - | Warning -> Flags.if_warn (fun () -> - msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () - | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) - -(* We provide a generic clear_log_backend callback for backends - wanting to do clenaup after the print. -*) -let std_logger_tag = ref None -let std_logger_cleanup = ref (fun () -> ()) - -let std_logger ?loc level msg = - gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; - !std_logger_cleanup () - -(* Rules for emacs: - - Debug/info: emacs_quote_info - - Warning/Error: emacs_quote_err - - Notice: unquoted - - Note the inconsistency. - *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None - -(** Color logging. Moved from pp_style, it may need some more refactoring *) - -(** Not thread-safe. We should put a lock somewhere if we print from - different threads. Do we? *) -let make_style_stack () = - (** Default tag is to reset everything *) - let empty = Terminal.make () in - let default_tag = Terminal.({ - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; - }) - in - let style_stack = ref [] in - let peek () = match !style_stack with - | [] -> default_tag (** Anomalous case, but for robustness *) - | st :: _ -> st - in - let push tag = - let style = match Ppstyle.get_style_format tag with - | None -> empty - | Some st -> st - 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 - style_stack := style :: !style_stack; - Terminal.eval style - in - let pop _ = match !style_stack with - | [] -> (** Something went wrong, we fallback *) - Terminal.eval default_tag - | _ :: rem -> style_stack := rem; - Terminal.eval (peek ()) - in - let clear () = style_stack := [] in - push, pop, clear - -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.to_format; - 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 - Format.pp_set_mark_tags !std_ft true; - Format.pp_set_mark_tags !err_ft true; - Format.pp_set_formatter_tag_functions !std_ft tag_handler; - Format.pp_set_formatter_tag_functions !err_ft tag_handler - -let logger = ref std_logger -let set_logger l = logger := l - -let msg_info ?loc x = !logger ?loc Info x -let msg_notice ?loc x = !logger ?loc Notice x -let msg_warning ?loc x = !logger ?loc Warning x -let msg_error ?loc x = !logger ?loc Error x -let msg_debug ?loc x = !logger ?loc Debug x - (** Feeders *) let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7 @@ -190,11 +56,6 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid -let debug_feeder = function - | { contents = Message (Debug, loc, pp) } -> - msg_debug ?loc (Pp.str (Richpp.raw_print pp)) - | _ -> () - let feedback_id = ref (Edit 0) let feedback_route = ref default_route @@ -209,32 +70,16 @@ let feedback ?id ?route what = } in Hashtbl.iter (fun _ f -> f m) feeders +(* Logging messages *) let feedback_logger ?loc lvl msg = - feedback ~route:!feedback_route ~id:!feedback_id - (Message (lvl, loc, Richpp.richpp_of_pp msg)) + feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg)) -(* Output to file *) -let ft_logger old_logger ft ?loc level mesg = - let id x = x in - match level with - | Debug -> msgnl_with ft (make_body id dbg_str mesg) - | Info -> msgnl_with ft (make_body id info_str mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ?loc level mesg - | Error -> old_logger ?loc level mesg - -let with_output_to_file fname func input = - let old_logger = !logger in - let channel = open_out (String.concat "." [fname; "out"]) in - logger := ft_logger old_logger (Format.formatter_of_out_channel channel); - try - let output = func input in - logger := old_logger; - close_out channel; - output - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - logger := old_logger; - close_out channel; - Exninfo.iraise reraise +let msg_info ?loc x = feedback_logger ?loc Info x +let msg_notice ?loc x = feedback_logger ?loc Notice x +let msg_warning ?loc x = feedback_logger ?loc Warning x +let msg_error ?loc x = feedback_logger ?loc Error x +let msg_debug ?loc x = feedback_logger ?loc Debug x +let debug_feeder = function + | { contents = Message (Debug, loc, pp) } -> msg_debug ?loc pp + | _ -> () diff --git a/lib/feedback.mli b/lib/feedback.mli index 8eae315883..3fb7c0039e 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -8,7 +8,7 @@ open Xml_datatype -(* Old plain messages (used to be in Pp) *) +(* Legacy-style logging messages (used to be in Pp) *) type level = | Debug | Info @@ -16,7 +16,6 @@ type level = | Warning | Error - (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int type state_id = Stateid.t @@ -44,7 +43,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Generic messages *) - | Message of level * Loc.t option * Richpp.richpp + | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { id : edit_or_state_id; (* The document part concerned *) @@ -53,32 +52,12 @@ type feedback = { } (** {6 Feedback sent, even asynchronously, to the user interface} *) - -(** Moved here from pp.ml *) - (* Morally the parser gets a string and an edit_id, and gives back an AST. * Feedbacks during the parsing phase are attached to this edit_id. * The interpreter assignes an exec_id to the ast, and feedbacks happening * during interpretation are attached to the exec_id. * Only one among state_id and edit_id can be provided. *) -(** A [logger] takes a level plus a pretty printing doc and logs it *) -type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit - -(** [set_logger l] makes the [msg_*] to use [l] for logging *) -val set_logger : logger -> unit - -(** [std_logger] standard logger to [stdout/stderr] *) -val std_logger : logger - -(** [init_color_output ()] Enable color in the std_logger *) -val init_color_output : unit -> unit - -(** [feedback_logger] will produce feedback messages instead IO events *) -val feedback_logger : logger -val emacs_logger : logger - - (** [add_feeder f] adds a feeder listiner [f], returning its id *) val add_feeder : (feedback -> unit) -> int @@ -97,10 +76,6 @@ val feedback : (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit -(** [with_output_to_file file f x] executes [f x] with logging - redirected to a file [file] *) -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b - (** {6 output functions} [msg_notice] do not put any decoration on output by default. If @@ -128,7 +103,3 @@ val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** For debugging purposes *) - - - - @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp_control - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -178,10 +176,9 @@ let pp_with ?pp_tag ft = | Ppcmd_glue sl -> List.iter pp_cmd sl | Ppcmd_string str -> let n = utf8_length str in pp_print_as ft n str - | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - cpp_open_box bty ; - if not (Format.over_max_boxes ()) then pp_cmd ss; - Format.pp_close_box ft () + | Ppcmd_box(bty,ss) -> cpp_open_box bty ; + if not (over_max_boxes ()) then pp_cmd ss; + pp_close_box ft () | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms diff --git a/lib/pp.mli b/lib/pp.mli index 5bf5391d3b..12747d3a1d 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -8,6 +8,30 @@ (** Coq document type. *) +(** Pretty printing guidelines ******************************************) +(* *) +(* std_ppcmds is the main pretty printing datatype in he Coq. Documents *) +(* are composed laying out boxes, and users can add arbitrary metadata *) +(* that backends are free to interpret. *) +(* *) +(* The datatype is public to allow serialization or advanced uses, *) +(* regular users are _strongly_ encouraged to use the top-level *) +(* functions to manipulate the type. *) +(* *) +(* Box order and number is indeed an important factor. Users should try *) +(* to create a proper amount of boxes. Also, the ++ operator provides *) +(* "efficient" concatenation, but directly using a list is preferred. *) +(* *) +(* That is to say, this: *) +(* *) +(* `hov [str "Term"; hov (pr_term t); str "is defined"]` *) +(* *) +(* is preferred to: *) +(* *) +(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")` *) +(* *) +(************************************************************************) + (* XXX: Improve and add attributes *) type pp_tag = string list diff --git a/lib/pp_control.ml b/lib/pp_control.ml deleted file mode 100644 index ab8dc0798c..0000000000 --- a/lib/pp_control.ml +++ /dev/null @@ -1,93 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Parameters of pretty-printing *) - -type pp_global_params = { - margin : int; - max_indent : int; - max_depth : int; - ellipsis : string } - -(* Default parameters of pretty-printing *) - -let dflt_gp = { - margin = 78; - max_indent = 50; - max_depth = 50; - ellipsis = "..." } - -(* A deeper pretty-printer to print proof scripts *) - -let deep_gp = { - margin = 78; - max_indent = 50; - max_depth = 10000; - ellipsis = "..." } - -(* set_gp : Format.formatter -> pp_global_params -> unit - * set the parameters of a formatter *) - -let set_gp ft gp = - Format.pp_set_margin ft gp.margin ; - Format.pp_set_max_indent ft gp.max_indent ; - Format.pp_set_max_boxes ft gp.max_depth ; - Format.pp_set_ellipsis_text ft gp.ellipsis - -let set_dflt_gp ft = set_gp ft dflt_gp - -let get_gp ft = - { margin = Format.pp_get_margin ft (); - max_indent = Format.pp_get_max_indent ft (); - max_depth = Format.pp_get_max_boxes ft (); - ellipsis = Format.pp_get_ellipsis_text ft () } - -(* with_fp : 'a pp_formatter_params -> Format.formatter - * returns of formatter for given formatter functions *) - -let with_fp chan out_function flush_function = - let ft = Format.make_formatter out_function flush_function in - Format.pp_set_formatter_out_channel ft chan; - ft - -(* Output on a channel ch *) - -let with_output_to ch = - let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in - set_gp ft deep_gp; - ft - -let std_ft = ref Format.std_formatter -let _ = set_dflt_gp !std_ft - -let err_ft = ref Format.err_formatter -let _ = set_gp !err_ft deep_gp - -let deep_ft = ref (with_output_to stdout) -let _ = set_gp !deep_ft deep_gp - -(* For parametrization through vernacular *) -let default = Format.pp_get_max_boxes !std_ft () -let default_margin = Format.pp_get_margin !std_ft () - -let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ()) -let set_depth_boxes v = - Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v) - -let get_margin () = Some (Format.pp_get_margin !std_ft ()) -let set_margin v = - let v = match v with None -> default_margin | Some v -> v in - Format.pp_set_margin Format.str_formatter v; - Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v; - (* Heuristic, based on usage: the column on the right of max_indent - column is 20% of width, capped to 30 characters *) - let m = max (64 * v / 100) (v-30) in - Format.pp_set_max_indent Format.str_formatter m; - Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m diff --git a/lib/pp_control.mli b/lib/pp_control.mli deleted file mode 100644 index d26f89eb30..0000000000 --- a/lib/pp_control.mli +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Parameters of pretty-printing. *) - -type pp_global_params = { - margin : int; - max_indent : int; - max_depth : int; - ellipsis : string } - -val dflt_gp : pp_global_params -val deep_gp : pp_global_params -val set_gp : Format.formatter -> pp_global_params -> unit -val set_dflt_gp : Format.formatter -> unit -val get_gp : Format.formatter -> pp_global_params - - -(** {6 Output functions of pretty-printing. } *) - -val with_output_to : out_channel -> Format.formatter - -val std_ft : Format.formatter ref -val err_ft : Format.formatter ref -val deep_ft : Format.formatter ref - -(** {6 For parametrization through vernacular. } *) - -val set_depth_boxes : int option -> unit -val get_depth_boxes : unit -> int option - -val set_margin : int option -> unit -val get_margin : unit -> int option diff --git a/lib/richpp.ml b/lib/richpp.ml deleted file mode 100644 index c0128dbc2d..0000000000 --- a/lib/richpp.ml +++ /dev/null @@ -1,200 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Xml_datatype - -type 'annotation located = { - annotation : 'annotation option; - startpos : int; - endpos : int -} - -type 'a stack = -| Leaf -| Node of string * 'a located gxml list * int * 'a stack - -type 'a context = { - mutable stack : 'a stack; - (** Pending opened nodes *) - mutable offset : int; - (** Quantity of characters printed so far *) - mutable annotations : 'a option Int.Map.t; - (** Map associating annotations to indexes *) - mutable index : int; - (** Current index of annotations *) -} - -(** We use Format to introduce tags inside the pretty-printed document. - Each inserted tag is a fresh index that we keep in sync with the contents - of annotations. - - We build an XML tree on the fly, by plugging ourselves in Format tag - marking functions. As those functions are called when actually writing to - the device, the resulting tree is correct. -*) -let rich_pp annotate ppcmds = - - let context = { - stack = Leaf; - offset = 0; - annotations = Int.Map.empty; - index = (-1); - } in - - let pp_tag obj = - let index = context.index + 1 in - let () = context.index <- index in - let obj = annotate obj in - let () = context.annotations <- Int.Map.add index obj context.annotations in - string_of_int index - in - - let pp_buffer = Buffer.create 180 in - - let push_pcdata () = - (** Push the optional PCData on the above node *) - let len = Buffer.length pp_buffer in - if len = 0 then () - else match context.stack with - | Leaf -> assert false - | Node (node, child, pos, ctx) -> - let data = Buffer.contents pp_buffer in - let () = Buffer.clear pp_buffer in - let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in - context.offset <- context.offset + len - in - - let open_xml_tag tag = - let () = push_pcdata () in - context.stack <- Node (tag, [], context.offset, context.stack) - in - - let close_xml_tag tag = - let () = push_pcdata () in - match context.stack with - | Leaf -> assert false - | Node (node, child, pos, ctx) -> - let () = assert (String.equal tag node) in - let annotation = - try Int.Map.find (int_of_string node) context.annotations - with _ -> None - in - let annotation = { - annotation = annotation; - startpos = pos; - endpos = context.offset; - } in - let xml = Element (node, annotation, List.rev child) in - match ctx with - | Leaf -> - (** Final node: we keep the result in a dummy context *) - context.stack <- Node ("", [xml], 0, Leaf) - | Node (node, child, pos, ctx) -> - context.stack <- Node (node, xml :: child, pos, ctx) - in - - let open Format in - - let ft = formatter_of_buffer pp_buffer in - - let tag_functions = { - mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); - mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); - print_open_tag = ignore; - print_close_tag = ignore; - } in - - pp_set_formatter_tag_functions ft tag_functions; - pp_set_mark_tags ft true; - - (* Set formatter width. This is currently a hack and duplicate code - with Pp_control. Hopefully it will be fixed better in Coq 8.7 *) - let w = pp_get_margin str_formatter () in - let m = max (64 * w / 100) (w-30) in - pp_set_margin ft w; - pp_set_max_indent ft m; - - (** The whole output must be a valid document. To that - end, we nest the document inside <pp> tags. *) - pp_open_tag ft "pp"; - Pp.(pp_with ~pp_tag ft ppcmds); - pp_close_tag ft (); - - (** Get the resulting XML tree. *) - let () = pp_print_flush ft () in - let () = assert (Buffer.length pp_buffer = 0) in - match context.stack with - | Node ("", [xml], 0, Leaf) -> xml - | _ -> assert false - - -let annotations_positions xml = - let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> - children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs - | _ -> - accu - and children accu cs = - List.fold_left node accu cs - in - node [] xml - -let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = - let rec node = function - | Element (index, { annotation; startpos; endpos }, cs) -> - let attributes = - [ "startpos", string_of_int startpos; - "endpos", string_of_int endpos - ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation - in - Element (tag, attributes, List.map node cs) - | PCData s -> - PCData s - in - node xml - -type richpp = xml - -let repr xml = xml -let richpp_of_xml xml = xml -let richpp_of_string s = PCData s - -let richpp_of_pp pp = - let annotate t = Some (Ppstyle.repr t) in - let rec drop = function - | PCData s -> [PCData s] - | Element (_, annotation, cs) -> - let cs = List.concat (List.map drop cs) in - match annotation.annotation with - | None -> cs - | Some s -> [Element (String.concat "." s, [], cs)] - in - let xml = rich_pp annotate pp in - Element ("_", [], drop xml) - -let raw_print xml = - let buf = Buffer.create 1024 in - let rec print = function - | PCData s -> Buffer.add_string buf s - | Element (_, _, cs) -> List.iter print cs - in - let () = print xml in - Buffer.contents buf - diff --git a/lib/richpp.mli b/lib/richpp.mli deleted file mode 100644 index 2e839e996b..0000000000 --- a/lib/richpp.mli +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This module offers semi-structured pretty-printing. *) - -(** Each annotation of the semi-structured document refers to the - substring it annotates. *) -type 'annotation located = { - annotation : 'annotation option; - startpos : int; - endpos : int -} - -(** [rich_pp get_annotations ppcmds] returns the interpretation - of [ppcmds] as a semi-structured document - that represents (located) annotations of this string. - The [get_annotations] function is used to convert tags into the desired - annotation. *) -val rich_pp : - (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> - 'annotation located Xml_datatype.gxml - -(** [annotations_positions ssdoc] returns a list associating each - annotations with its position in the string from which [ssdoc] is - built. *) -val annotations_positions : - 'annotation located Xml_datatype.gxml -> - ('annotation * (int * int)) list - -(** [xml_of_rich_pp ssdoc] returns an XML representation of the - semi-structured document [ssdoc]. *) -val xml_of_rich_pp : - ('annotation -> string) -> - ('annotation -> (string * string) list) -> - 'annotation located Xml_datatype.gxml -> - Xml_datatype.xml - -(** {5 Enriched text} *) - -type richpp -(** Type of text with style annotations *) - -val richpp_of_pp : Pp.std_ppcmds -> richpp -(** Extract style information from formatted text *) - -val richpp_of_xml : Xml_datatype.xml -> richpp -(** Do not use outside of dedicated areas *) - -val richpp_of_string : string -> richpp -(** Make a styled text out of a normal string *) - -val repr : richpp -> Xml_datatype.xml -(** Observe the styled text as XML *) - -(** {5 Debug/Compat} *) - -(** Represent the semi-structured document as a string, dropping any additional - information. *) -val raw_print : richpp -> string |