From 777f0ace3d2458cbe1840dcf3d8f350452721e84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Feb 2015 09:30:53 +0100
Subject: Removing dead code.
---
lib/monad.ml | 2 +-
lib/pp.ml | 2 --
2 files changed, 1 insertion(+), 3 deletions(-)
(limited to 'lib')
diff --git a/lib/monad.ml b/lib/monad.ml
index 4a52684da4..a1714a41b3 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 234d2344f6..cc56e5e8d7 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))
--
cgit v1.2.3
From ab97dd2c8d49e59b7fb623e1fe9606395a176187 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 4 Feb 2015 11:36:05 +0100
Subject: CThread: workaround for threads lockup on windwos made more
aggressive
---
lib/cThread.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
(limited to 'lib')
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 55bb6fd6d0..84e5ae4fe6 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 ()
--
cgit v1.2.3
From bfe40c0f8bbb13c7aceb686c8102b17ff8291d8b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 4 Feb 2015 13:24:03 +0100
Subject: More efficient implementation of Richpp.
Instead of constructing the XML string and parsing it afterwards,
we build it by hijacking the formatting output.
---
lib/richpp.ml | 130 +++++++++++++++++++++++++++++-----------------------------
1 file changed, 64 insertions(+), 66 deletions(-)
(limited to 'lib')
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 745b7d2a22..442050cf89 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,12 +15,18 @@ type 'annotation located = {
endpos : int
}
-let rich_pp annotate ppcmds =
- (** First, we use Format to introduce tags inside
- the pretty-printed document.
+type context =
+| Leaf
+| Node of string * xml list * context
+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.
+
+ 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 annotations = ref [] in
let index = ref (-1) in
@@ -29,58 +36,67 @@ let rich_pp annotate ppcmds =
string_of_int !index
in
- let tagged_pp = Format.(
+ let pp_buffer = Buffer.create 13 in
- (** Warning: The following instructions are valid only if
- [str_formatter] is not used for another purpose in
- Pp.pp_with. *)
+ let push_pcdata context =
+ (** Push the optional PCData on the above node *)
+ if (Buffer.length pp_buffer = 0) then ()
+ else match !context with
+ | Leaf -> assert false
+ | Node (node, child, ctx) ->
+ let data = Buffer.contents pp_buffer in
+ let () = Buffer.clear pp_buffer in
+ context := Node (node, PCData data :: child, ctx)
+ in
- let ft = str_formatter in
+ let open_xml_tag context tag =
+ let () = push_pcdata context in
+ context := Node (tag, [], !context)
+ in
- (** We reuse {!Format} standard way of producing tags
- inside pretty-printing. *)
- pp_set_tags ft true;
+ let close_xml_tag context tag =
+ let () = push_pcdata context in
+ match !context with
+ | Leaf -> assert false
+ | Node (node, child, ctx) ->
+ let () = assert (String.equal tag node) in
+ let xml = Element (node, [], List.rev child) in
+ match ctx with
+ | Leaf ->
+ (** Final node: we keep the result in a dummy context *)
+ context := Node ("", [xml], Leaf)
+ | Node (node, child, ctx) ->
+ context := Node (node, xml :: child, ctx)
+ in
- (** The whole output must be a valid document. To that
- end, we nest the document inside a tag named . *)
- pp_open_tag ft "pp";
+ let xml_pp = Format.(
- (** 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.
+ let ft = formatter_of_buffer pp_buffer in
- 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 . *)
+ let context = ref Leaf in
+
+ let tag_functions = {
+ mark_open_tag = (fun tag -> let () = open_xml_tag context tag in "");
+ mark_close_tag = (fun tag -> let () = close_xml_tag context 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 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
+ (** Get the resulting XML tree. *)
+ let () = pp_print_flush ft () in
+ let () = assert (Buffer.length pp_buffer = 0) in
+ match !context with
+ | Node ("", [xml], Leaf) -> xml
+ | _ -> assert false
)
in
(** Second, we retrieve the final function that relates
@@ -88,24 +104,7 @@ let rich_pp annotate ppcmds =
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
- in
-
- (** Fourth, the low-level XML is turned into a high-level
+ (** Third, 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. *)
@@ -132,7 +131,6 @@ let rich_pp annotate ppcmds =
in
(startpos, endpos, List.rev cs)
in
- let pp_buffer = Buffer.create 13 in
let xml, _ = node pp_buffer xml_pp in
(** We return the raw pretty-printing and its annotations tree. *)
--
cgit v1.2.3
From ac73048656780b6f02d303daf2c59883c9346eb7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 4 Feb 2015 15:45:29 +0100
Subject: Marshal.from_string on 32 bit systems use tmpfile if needed (Close:
3968)
Strings are at most 16M on 32 bit OCaml, and the system state
may be bigger. In this case we write to tmp file and
Marshal.from_channel. We can't directly use the channel interface
because of badly designed non blocking API (available only on fds and
not channels).
---
lib/cThread.ml | 39 ++++++++++++++++++++++++++++++++++-----
1 file changed, 34 insertions(+), 5 deletions(-)
(limited to 'lib')
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 84e5ae4fe6..2d1f10bf39 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -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
--
cgit v1.2.3
From cdfb6705e0a2d01b7c01d83bfe898a64ee148c34 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Feb 2015 21:35:36 +0100
Subject: More efficient Richpp.
We build the rich XML at once without generating the printed string.
---
lib/richpp.ml | 173 +++++++++++++++++++++++++++------------------------------
lib/richpp.mli | 4 +-
2 files changed, 84 insertions(+), 93 deletions(-)
(limited to 'lib')
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 442050cf89..c4a9c39d5a 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -15,126 +15,117 @@ type 'annotation located = {
endpos : int
}
-type context =
+type 'a stack =
| Leaf
-| Node of string * xml list * context
+| 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.
-
- 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 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 context =
+ let push_pcdata () =
(** Push the optional PCData on the above node *)
- if (Buffer.length pp_buffer = 0) then ()
- else match !context with
+ let len = Buffer.length pp_buffer in
+ if len = 0 then ()
+ else match context.stack with
| Leaf -> assert false
- | Node (node, child, ctx) ->
+ | Node (node, child, pos, ctx) ->
let data = Buffer.contents pp_buffer in
let () = Buffer.clear pp_buffer in
- context := Node (node, PCData data :: child, ctx)
+ let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in
+ context.offset <- context.offset + len
in
- let open_xml_tag context tag =
- let () = push_pcdata context in
- context := Node (tag, [], !context)
+ let open_xml_tag tag =
+ let () = push_pcdata () in
+ context.stack <- Node (tag, [], context.offset, context.stack)
in
- let close_xml_tag context tag =
- let () = push_pcdata context in
- match !context with
+ let close_xml_tag tag =
+ let () = push_pcdata () in
+ match context.stack with
| Leaf -> assert false
- | Node (node, child, ctx) ->
+ | Node (node, child, pos, ctx) ->
let () = assert (String.equal tag node) in
- let xml = Element (node, [], List.rev child) 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 := Node ("", [xml], Leaf)
- | Node (node, child, ctx) ->
- context := Node (node, xml :: child, ctx)
+ context.stack <- Node ("", [xml], 0, Leaf)
+ | Node (node, child, pos, ctx) ->
+ context.stack <- Node (node, xml :: child, pos, ctx)
in
- let xml_pp = Format.(
-
- let ft = formatter_of_buffer pp_buffer in
+ let open Format in
- let context = ref Leaf in
+ let ft = formatter_of_buffer pp_buffer in
- let tag_functions = {
- mark_open_tag = (fun tag -> let () = open_xml_tag context tag in "");
- mark_close_tag = (fun tag -> let () = close_xml_tag context tag in "");
- print_open_tag = ignore;
- print_close_tag = ignore;
- } 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;
+ 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 ();
+ (** 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 with
- | Node ("", [xml], Leaf) -> xml
- | _ -> assert false
- )
- 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, 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)
-
- | PCData s ->
- Buffer.add_string buffer s;
- (PCData s, Buffer.length buffer)
-
- | _ ->
- 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 xml, _ = node pp_buffer xml_pp in
+ (** 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 446ee1a046..bf80c8dc8c 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
--
cgit v1.2.3
From a71aec672bc66a0e19752fa15d55bc2bd75ef3bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 7 Feb 2015 15:21:14 +0100
Subject: Fixing bug #4009.
We only allow color output under Unix OSes.
---
lib/terminal.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
(limited to 'lib')
diff --git a/lib/terminal.ml b/lib/terminal.ml
index 1e6c25578e..0f6b23af36 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