From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- lib/cArray.ml | 28 ++++---- lib/cArray.mli | 5 ++ lib/cString.ml | 9 ++- lib/cThread.ml | 41 +++++++++-- lib/dyn.ml | 2 + lib/dyn.mli | 1 + lib/errors.ml | 2 +- lib/errors.mli | 2 +- lib/future.ml | 72 ++++++++++--------- lib/future.mli | 5 +- lib/hashcons.ml | 3 + lib/hashcons.mli | 2 + lib/hashset.ml | 26 +++++++ lib/hashset.mli | 9 +++ lib/monad.ml | 2 +- lib/pp.ml | 13 +++- lib/richpp.ml | 215 ++++++++++++++++++++++++++----------------------------- lib/richpp.mli | 4 +- lib/terminal.ml | 3 +- 19 files changed, 267 insertions(+), 177 deletions(-) (limited to 'lib') diff --git a/lib/cArray.ml b/lib/cArray.ml index 16034543..bb1e3354 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -13,6 +13,7 @@ sig include S val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool + val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool val is_empty : 'a array -> bool val exists : ('a -> bool) -> 'a array -> bool val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool @@ -85,19 +86,22 @@ let compare cmp v1 v2 = in loop (len - 1) +let equal_norefl cmp t1 t2 = + let len = Array.length t1 in + if not (Int.equal len (Array.length t2)) then false + else + let rec aux i = + if i < 0 then true + else + let x = uget t1 i in + let y = uget t2 i in + cmp x y && aux (pred i) + in + aux (len - 1) + let equal cmp t1 t2 = - if t1 == t2 then true else - let len = Array.length t1 in - if not (Int.equal len (Array.length t2)) then false - else - let rec aux i = - if i < 0 then true - else - let x = uget t1 i in - let y = uget t2 i in - cmp x y && aux (pred i) - in - aux (len - 1) + if t1 == t2 then true else equal_norefl cmp t1 t2 + let is_empty array = Int.equal (Array.length array) 0 diff --git a/lib/cArray.mli b/lib/cArray.mli index 39c35e2d..7e5c93b5 100644 --- a/lib/cArray.mli +++ b/lib/cArray.mli @@ -17,6 +17,11 @@ sig val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool (** Lift equality to array type. *) + val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool + (** Like {!equal} but does not assume that equality is reflexive: no + optimisation is performed if both arrays are physically the + same. *) + val is_empty : 'a array -> bool (** True whenever the array is empty. *) diff --git a/lib/cString.ml b/lib/cString.ml index 250b7cee..e9006860 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -135,7 +135,14 @@ let plural n s = if n<>1 then s^"s" else s let conjugate_verb_to_be n = if n<>1 then "are" else "is" let ordinal n = - let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in + let s = + if (n / 10) mod 10 = 1 then "th" + else match n mod 10 with + | 1 -> "st" + | 2 -> "nd" + | 3 -> "rd" + | _ -> "th" + in string_of_int n ^ s (* string parsing *) diff --git a/lib/cThread.ml b/lib/cThread.ml index 55bb6fd6..2d1f10bf 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -22,7 +22,7 @@ let thread_friendly_read_fd fd s ~off ~len = let rec loop () = try Unix.read fd s off len with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) -> - while not (safe_wait_timed_read fd 1.0) do Thread.yield () done; + while not (safe_wait_timed_read fd 0.05) do Thread.yield () done; loop () in loop () @@ -43,6 +43,18 @@ let really_read_fd fd s off len = i := !i + r done +let really_read_fd_2_oc fd oc len = + let i = ref 0 in + let size = 4096 in + let s = String.create size in + while !i < len do + let len = len - !i in + let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in + if r = 0 then raise End_of_file; + i := !i + r; + output oc s 0 r; + done + let thread_friendly_really_read ic s ~off ~len = try let fd = Unix.descr_of_in_channel ic in @@ -68,9 +80,26 @@ let thread_friendly_input_value ic = let header = String.create Marshal.header_size in really_read_fd fd header 0 Marshal.header_size; let body_size = Marshal.data_size header 0 in - let msg = String.create (body_size + Marshal.header_size) in - String.blit header 0 msg 0 Marshal.header_size; - really_read_fd fd msg Marshal.header_size body_size; - Marshal.from_string msg 0 - with Unix.Unix_error _ -> raise End_of_file + let desired_size = body_size + Marshal.header_size in + if desired_size <= Sys.max_string_length then begin + let msg = String.create desired_size in + String.blit header 0 msg 0 Marshal.header_size; + really_read_fd fd msg Marshal.header_size body_size; + Marshal.from_string msg 0 + end else begin + (* Workaround for 32 bit systems and data > 16M *) + let name, oc = + Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in + try + output oc header 0 Marshal.header_size; + really_read_fd_2_oc fd oc body_size; + close_out oc; + let ic = open_in_bin name in + let data = Marshal.from_channel ic in + close_in ic; + Sys.remove name; + data + with e -> Sys.remove name; raise e + end + with Unix.Unix_error _ | Sys_error _ -> raise End_of_file diff --git a/lib/dyn.ml b/lib/dyn.ml index 63def9a1..a5e8fb9c 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -47,3 +47,5 @@ let tag (s,_) = anomaly msg let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 + +let dump () = Int.Map.bindings !dyntab diff --git a/lib/dyn.mli b/lib/dyn.mli index 4a713472..cac912ac 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -14,3 +14,4 @@ val create : string -> ('a -> t) * (t -> 'a) val tag : t -> string val has_tag : t -> string -> bool val pointer_equal : t -> t -> bool +val dump : unit -> (int * string) list diff --git a/lib/errors.ml b/lib/errors.ml index ab331d6a..a4ec357e 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -108,7 +108,7 @@ let _ = register_handler begin function | _ -> raise Unhandled end -(** Critical exceptions shouldn't be catched and ignored by mistake +(** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled only at the very end of interp, to be displayed to the user. *) diff --git a/lib/errors.mli b/lib/errors.mli index e4096a7e..03caa6a9 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -81,7 +81,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds isn't printed (used in Ltac debugging). *) val print_no_report : exn -> Pp.std_ppcmds -(** Critical exceptions shouldn't be catched and ignored by mistake +(** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user. Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... diff --git a/lib/future.ml b/lib/future.ml index 2f1ce5e4..02d3702d 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -11,19 +11,21 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g -exception NotReady -exception NotHere +exception NotReady of string +exception NotHere of string let _ = Errors.register_handler (function - | NotReady -> - Pp.strbrk("The value you are asking for is not ready yet. " ^ + | NotReady name -> + Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing.") - | NotHere -> - Pp.strbrk("The value you are asking for is not available "^ + "asynchronous script processing and don't pass \"-quick\" to "^ + "coqc.") + | NotHere name -> + Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing.") + "asynchronous script processing and don't pass \"-quick\" to "^ + "coqc.") | _ -> raise Errors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn @@ -54,67 +56,69 @@ and 'a comp = | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = - | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key + | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key | Finished of 'a and 'a computation = 'a comput ref -let create ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (Ephemeron.create (uuid, f, Pervasives.ref x))) +let unnamed = "unnamed" + +let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = + ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with - | Finished v -> UUID.invalid, id, ref (Val (v,None)) - | Ongoing x -> - try Ephemeron.get x + | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) + | Ongoing (name, x) -> + try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c with Ephemeron.InvalidKey -> - UUID.invalid, id, ref (Exn (NotHere, Exninfo.null)) + name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null)) type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] -let is_over kx = let _, _, x = get kx in match !x with +let is_over kx = let _, _, _, x = get kx in match !x with | Val _ | Exn _ -> true | Closure _ | Delegated _ -> false -let is_val kx = let _, _, x = get kx in match !x with +let is_val kx = let _, _, _, x = get kx in match !x with | Val _ -> true | Exn _ | Closure _ | Delegated _ -> false -let is_exn kx = let _, _, x = get kx in match !x with +let is_exn kx = let _, _, _, x = get kx in match !x with | Exn _ -> true | Val _ | Closure _ | Delegated _ -> false -let peek_val kx = let _, _, x = get kx in match !x with +let peek_val kx = let _, _, _, x = get kx in match !x with | Val (v, _) -> Some v | Exn _ | Closure _ | Delegated _ -> None -let uuid kx = let id, _, _ = get kx in id +let uuid kx = let _, id, _, _ = get kx in id let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) -let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn +let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn -let create_delegate ?(blocking=true) fix_exn = +let create_delegate ?(blocking=true) ~name fix_exn = let assignement signal ck = fun v -> - let _, fix_exn, c = get ck in + let _, _, fix_exn, c = get ck in assert (match !c with Delegated _ -> true | _ -> false); begin match v with | `Val v -> c := Val (v, None) | `Exn e -> c := Exn (fix_exn e) - | `Comp f -> let _, _, comp = get f in c := !comp end; + | `Comp f -> let _, _, _, comp = get f in c := !comp end; signal () in let wait, signal = - if not blocking then (fun () -> raise NotReady), ignore else + if not blocking then (fun () -> raise (NotReady name)), ignore else let lock = Mutex.create () in let cond = Condition.create () in (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in - let ck = create fix_exn (Delegated wait) in + let ck = create ~name fix_exn (Delegated wait) in ck, assignement signal ck (* TODO: get rid of try/catch to be stackless *) let rec compute ~pure ck : 'a value = - let _, fix_exn, c = get ck in + let _, _, fix_exn, c = get ck in match !c with | Val (x, _) -> `Val x | Exn (e, info) -> `Exn (e, info) @@ -128,7 +132,7 @@ let rec compute ~pure ck : 'a value = let e = Errors.push e in let e = fix_exn e in match e with - | (NotReady, _) -> `Exn e + | (NotReady _, _) -> `Exn e | _ -> c := Exn e; `Exn e let force ~pure x = match compute ~pure x with @@ -136,8 +140,8 @@ let force ~pure x = match compute ~pure x with | `Exn e -> Exninfo.iraise e let chain ~pure ck f = - let uuid, fix_exn, c = get ck in - create ~uuid fix_exn (match !c with + let name, uuid, fix_exn, c = get ck in + create ~uuid ~name fix_exn (match !c with | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) | Exn _ as x -> x | Val (v, None) when pure -> Closure (fun () -> f v) @@ -156,7 +160,7 @@ let chain ~pure ck f = let create fix_exn f = create fix_exn (Closure f) let replace kx y = - let _, _, x = get kx in + let _, _, _, x = get kx in match !x with | Exn _ -> x := Closure (fun () -> force ~pure:false y) | _ -> Errors.anomaly @@ -207,10 +211,10 @@ let map2 ?greedy f x l = let print f kx = let open Pp in - let (uid, _, x) = get kx in + let name, uid, _, x = get kx in let uid = - if UUID.equal uid UUID.invalid then str "[#]" - else str "[" ++ int uid ++ str "]" + if UUID.equal uid UUID.invalid then str "[#:" ++ str name ++ str "]" + else str "[" ++ int uid ++ str":" ++ str name ++ str "]" in match !x with | Delegated _ -> str "Delegated" ++ uid diff --git a/lib/future.mli b/lib/future.mli index 8a4fa0bd..324d5f7d 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -63,7 +63,7 @@ end module UUIDMap : Map.S with type key = UUID.t module UUIDSet : Set.S with type elt = UUID.t -exception NotReady +exception NotReady of string type 'a computation type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] @@ -100,7 +100,8 @@ val fix_exn_of : 'a computation -> fix_exn delage assigns it. *) type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] val create_delegate : - ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit) + ?blocking:bool -> name:string -> + fix_exn -> 'a computation * ('a assignement -> unit) (* Given a computation that is_exn, replace it by another one *) val replace : 'a computation -> 'a computation -> unit diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 752e2634..46ba0b62 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -43,6 +43,7 @@ module type S = type table val generate : u -> table val hcons : table -> t -> t + val stats : table -> Hashset.statistics end module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = @@ -67,6 +68,8 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = let y = X.hashcons u x in Htbl.repr (X.hash y) y tab + let stats (tab, _) = Htbl.stats tab + end (* A few usefull wrappers: diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 60a9ee01..8d0adc3f 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -56,6 +56,8 @@ module type S = (** This create a hashtable of the hashconsed objects. *) val hcons : table -> t -> t (** Perform the hashconsing of the given object within the table. *) + val stats : table -> Hashset.statistics + (** Recover statistics of the hashconsing table. *) end module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) diff --git a/lib/hashset.ml b/lib/hashset.ml index 6bec81c7..1ca6cc64 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -19,12 +19,20 @@ module type EqType = sig val equal : t -> t -> bool end +type statistics = { + num_bindings: int; + num_buckets: int; + max_bucket_length: int; + bucket_histogram: int array +} + module type S = sig type elt type t val create : int -> t val clear : t -> unit val repr : int -> elt -> t -> elt + val stats : t -> statistics end module Make (E : EqType) = @@ -185,6 +193,24 @@ module Make (E : EqType) = let ifnotfound index = add_aux t Weak.set (Some d) h index; d in find_or h t d ifnotfound + let stats t = + let fold accu bucket = max (count_bucket 0 bucket 0) accu in + let max_length = Array.fold_left fold 0 t.table in + let histogram = Array.make (max_length + 1) 0 in + let iter bucket = + let len = count_bucket 0 bucket 0 in + histogram.(len) <- succ histogram.(len) + in + let () = Array.iter iter t.table in + let fold (num, len, i) k = (num + k * i, len + k, succ i) in + let (num, len, _) = Array.fold_left fold (0, 0, 0) histogram in + { + num_bindings = num; + num_buckets = len; + max_bucket_length = Array.length histogram; + bucket_histogram = histogram; + } + end module Combine = struct diff --git a/lib/hashset.mli b/lib/hashset.mli index 537f3418..a455eec6 100644 --- a/lib/hashset.mli +++ b/lib/hashset.mli @@ -19,6 +19,13 @@ module type EqType = sig val equal : t -> t -> bool end +type statistics = { + num_bindings: int; + num_buckets: int; + max_bucket_length: int; + bucket_histogram: int array +} + module type S = sig type elt (** Type of hashsets elements. *) @@ -34,6 +41,8 @@ module type S = sig specific representation that is stored in [set]. Otherwise, [constr] is stored in [set] and will be used as the canonical representation of this value in the future. *) + val stats : t -> statistics + (** Recover statistics on the table. *) end module Make (E : EqType) : S with type elt = E.t diff --git a/lib/monad.ml b/lib/monad.ml index 4a52684d..a1714a41 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -111,7 +111,7 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | [a] -> M.map (fun a' -> [a']) (f a) | a::b::l -> - map f l >>= fun l' -> + map_right f l >>= fun l' -> f b >>= fun b' -> M.map (fun a' -> a'::b'::l') (f a) diff --git a/lib/pp.ml b/lib/pp.ml index 234d2344..76046a7f 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -387,8 +387,6 @@ let pp_with ?pp_tag ft strm = let ppnl_with ft strm = pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ()))) -let pp_flush_with ft = Format.pp_print_flush ft - (* pretty printing functions WITH FLUSH *) let msg_with ft strm = pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) @@ -519,8 +517,17 @@ let pr_arg pr x = 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 +(** TODO: merge with CString.ordinal *) let pr_nth n = - int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th") + let s = + if (n / 10) mod 10 = 1 then "th" + else match n mod 10 with + | 1 -> "st" + | 2 -> "nd" + | 3 -> "rd" + | _ -> "th" + in + int n ++ str s (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) diff --git a/lib/richpp.ml b/lib/richpp.ml index 745b7d2a..c4a9c39d 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Xml_datatype type 'annotation located = { @@ -14,129 +15,117 @@ type 'annotation located = { 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 = - (** First, 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. - *) - let annotations = ref [] in - let index = ref (-1) in + + let context = { + stack = Leaf; + offset = 0; + annotations = Int.Map.empty; + index = (-1); + } in + let pp_tag obj = - let () = incr index in - let () = annotations := obj :: !annotations in - string_of_int !index + 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 13 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 tagged_pp = Format.( - - (** Warning: The following instructions are valid only if - [str_formatter] is not used for another purpose in - Pp.pp_with. *) - - let ft = str_formatter in - - (** We reuse {!Format} standard way of producing tags - inside pretty-printing. *) - pp_set_tags ft true; - - (** The whole output must be a valid document. To that - end, we nest the document inside a tag named . *) - pp_open_tag ft "pp"; - - (** XML ignores spaces. The problem is that our pretty-printings - are based on spaces to indent. To solve that problem, we - systematically output non-breakable spaces, which are properly - honored by XML. - - To do so, we reconfigure the [str_formatter] temporarily by - hijacking the function that output spaces. *) - let out, flush, newline, std_spaces = - pp_get_all_formatter_output_functions ft () - in - let set = pp_set_all_formatter_output_functions ft ~out ~flush ~newline in - set ~spaces:(fun k -> - for i = 0 to k - 1 do - Buffer.add_string stdbuf " " - done - ); - - (** Some characters must be escaped in XML. This is done by the - following rewriting of the strings held by pretty-printing - commands. *) - Pp.(pp_with ~pp_tag ft (rewrite Xml_printer.pcdata_to_string ppcmds)); - - (** Insert . *) - pp_close_tag ft (); - - (** Get the final string. *) - let output = flush_str_formatter () in - - (** Finalize by restoring the state of the [str_formatter] and the - default behavior of Format. By the way, there may be a bug here: - there is no {!Format.pp_get_tags} and therefore if the tags flags - was already set to true before executing this piece of code, the - state of Format is not restored. *) - set ~spaces:std_spaces; - pp_set_tags ft false; - output - ) + let open_xml_tag tag = + let () = push_pcdata () in + context.stack <- Node (tag, [], context.offset, context.stack) in - (** Second, we retrieve the final function that relates - each tag to an annotation. *) - let objs = CArray.rev_of_list !annotations in - let get index = annotate objs.(index) in - - (** Third, we parse the resulting string. It is a valid XML - document (in the sense of Xml_parser). As blanks are - meaningful we deactivate canonicalization in the XML - parser. *) - let xml_pp = - try - Xml_parser.(parse ~do_not_canonicalize:true (make (SString tagged_pp))) - with Xml_parser.Error e -> - Printf.eprintf - "Broken invariant (RichPp): \n\ - The output semi-structured pretty-printing is ill-formed.\n\ - Please report.\n\ - %s" - (Xml_parser.error e); - exit 1 + + 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 - (** Fourth, the low-level XML is turned into a high-level - semi-structured document that contains a located annotation in - every node. During the traversal of the low-level XML document, - we build a raw string representation of the pretty-print. *) - let rec node buffer = function - | Element (index, [], cs) -> - let startpos, endpos, cs = children buffer cs in - let annotation = try get (int_of_string index) with _ -> None in - (Element (index, { annotation; startpos; endpos }, cs), endpos) + let open Format in - | PCData s -> - Buffer.add_string buffer s; - (PCData s, Buffer.length buffer) + let ft = formatter_of_buffer pp_buffer in - | _ -> - assert false (* Because of the form of XML produced by Format. *) - - and children buffer cs = - let startpos = Buffer.length buffer in - let cs, endpos = - List.fold_left (fun (cs, endpos) c -> - let c, endpos = node buffer c in - (c :: cs, endpos) - ) ([], startpos) cs - in - (startpos, endpos, List.rev cs) - in - let pp_buffer = Buffer.create 13 in - let xml, _ = node pp_buffer xml_pp 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; + + (** The whole output must be a valid document. To that + end, we nest the document inside 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 - (** We return the raw pretty-printing and its annotations tree. *) - (Buffer.contents pp_buffer, xml) let annotations_positions xml = let rec node accu = function diff --git a/lib/richpp.mli b/lib/richpp.mli index 446ee1a0..bf80c8dc 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -17,13 +17,13 @@ type 'annotation located = { } (** [rich_pp get_annotations ppcmds] returns the interpretation - of [ppcmds] as a string as well as a semi-structured document + 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. If this function returns [None], then no annotation is put. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - string * 'annotation located Xml_datatype.gxml + 'annotation located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is diff --git a/lib/terminal.ml b/lib/terminal.ml index 1e6c2557..0f6b23af 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -167,7 +167,8 @@ let reset_style = { negative = Some false; } -let has_style t = Unix.isatty t +let has_style t = + Unix.isatty t && Sys.os_type = "Unix" let split c s = let len = String.length s in -- cgit v1.2.3