diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /lib/pp.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 77 |
1 files changed, 44 insertions, 33 deletions
@@ -8,13 +8,9 @@ module Glue : sig - (* A left associative glue implements efficient glue operator - when used as left associative. If glue is denoted ++ then + (** The [Glue] module implements a container data structure with + efficient concatenation. *) - a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @ [a])) - - I.e. if the short list is the second argument - *) type 'a t val atom : 'a -> 'a t @@ -22,19 +18,28 @@ module Glue : sig val empty : 'a t val is_empty : 'a t -> bool val iter : ('a -> unit) -> 'a t -> unit - val map : ('a -> 'b) -> 'a t -> 'b t end = struct - type 'a t = 'a list + type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t + + let atom x = GLeaf x + + let glue x y = + match x, y with + | GEmpty, _ -> y + | _, GEmpty -> x + | _, _ -> GNode (x,y) + + let empty = GEmpty - let atom x = [x] - let glue x y = y @ x - let empty = [] - let is_empty x = x = [] + let is_empty x = x = GEmpty + + let rec iter f = function + | GEmpty -> () + | GLeaf x -> f x + | GNode (x,y) -> iter f x; iter f y - let iter f g = List.iter f (List.rev g) - let map = List.map end module Tag : @@ -145,21 +150,6 @@ let app = Glue.glue let is_empty g = Glue.is_empty g -let rewrite f p = - let strtoken = function - | Str_len (s, n) -> - let s' = f s in - Str_len (s', String.length s') - | Str_def s -> - Str_def (f s) - in - let rec ppcmd_token = function - | Ppcmd_print x -> Ppcmd_print (strtoken x) - | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g) - | p -> p - in - Glue.map ppcmd_token p - (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is @@ -259,7 +249,7 @@ let escape_string s = else escape_at s (i-1) in escape_at s (String.length s - 1) -let qstring s = str ("\""^escape_string s^"\"") +let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring let quote s = h 0 (str "\"" ++ s ++ str "\"") @@ -372,11 +362,11 @@ let emacs_quote_info_start = "<infomsg>" let emacs_quote_info_end = "</infomsg>" 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 @@ -434,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 @@ -458,6 +448,27 @@ let logger = ref std_logger let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger let make_pp_nonemacs() = print_emacs:=false; logger := std_logger +let ft_logger old_logger ft ~id level mesg = match level with + | Debug _ -> msgnl_with ft (debugbody mesg) + | Info -> msgnl_with ft (infobody mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger ~id:id level mesg + | Error -> old_logger ~id:id 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 feedback_id = ref (Feedback.Edit 0) let feedback_route = ref Feedback.default_route |