diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in index cf09ddd667ed096ced79582ad7905f8ddc82ed19..f9f3b85e50c177faaf67b5284c35f1d8ad658ae9 100644 --- a/src/libraries/stdlib/transitioning.ml.in +++ b/src/libraries/stdlib/transitioning.ml.in @@ -29,6 +29,7 @@ module Stdlib = struct let max = max let min_int = min_int let max_int = max_int + let flush = flush end [@@@ warning "-3"] diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli index 94ae54311a9ca97d31b0eab45927b7d4454c96c8..6e75b7538adbef2250caf22ada530f099a6d9b54 100644 --- a/src/libraries/stdlib/transitioning.mli +++ b/src/libraries/stdlib/transitioning.mli @@ -42,6 +42,7 @@ module Stdlib: sig val max: 'a -> 'a -> 'a val min_int: int val max_int: int + val flush: out_channel -> unit end (** 4.08 *) diff --git a/src/libraries/utils/dotgraph.ml b/src/libraries/utils/dotgraph.ml index f9939a2eb3677e29cafc5c34cbdbcbcefc2e07ef..1eea4ded519a8389b71a3803c82717b4e33c43d2 100644 --- a/src/libraries/utils/dotgraph.ml +++ b/src/libraries/utils/dotgraph.ml @@ -128,7 +128,7 @@ let close dot = begin Format.fprintf dot.fmt "}@." ; dot.fmt <- Format.err_formatter ; - Pervasives.flush out ; close_out out ; + Transitioning.Stdlib.flush out ; close_out out ; dot.out <- None ; end diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml index f09e17a02370c98549ba9f15a30a20b64bc2b0c6..1c382c45bcc4f9f3b29ff1a7767a16fc5adb16a5 100644 --- a/src/plugins/server/doc.ml +++ b/src/plugins/server/doc.ml @@ -123,7 +123,7 @@ let table_of_contents () = module Cmap = Map.Make (struct type t = string list - let compare = Pervasives.compare + let compare = Transitioning.Stdlib.compare end) let index_entry (title,href) = diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml index 70e5d66af55ac68ad3b4d464a644f168d18f6073..d354dc8bc22d5c498edde315774d822fb376289b 100644 --- a/src/plugins/server/jbuffer.ml +++ b/src/plugins/server/jbuffer.ml @@ -40,7 +40,8 @@ let flush buffer () = buffer.rjson <- js :: buffer.rjson ; FCBuffer.clear t -let push_tag buffer tag = +let push_tag buffer stag = + let tag = Transitioning.Format.string_of_stag stag in flush buffer () ; buffer.stack <- ( tag , buffer.rjson ) :: buffer.stack ; buffer.rjson <- [] @@ -83,15 +84,15 @@ let create ?indent ?margin () = Format.pp_set_max_indent fmt (max 0 (min k (m-10))) end ; begin - let open Format in - pp_set_formatter_tag_functions fmt { - print_open_tag = no_mark ; - print_close_tag = no_mark ; - mark_open_tag = mark_open_tag buffer ; - mark_close_tag = mark_close_tag buffer ; + let open Transitioning.Format in + pp_set_formatter_stag_functions fmt { + print_open_stag = no_mark ; + print_close_stag = no_mark ; + mark_open_stag = mark_open_tag buffer ; + mark_close_stag = mark_close_tag buffer ; } ; - pp_set_print_tags fmt false ; - pp_set_mark_tags fmt true ; + Format.pp_set_print_tags fmt false ; + Format.pp_set_mark_tags fmt true ; end ; buffer diff --git a/src/plugins/server/jbuffer.mli b/src/plugins/server/jbuffer.mli index 3e1e02a1beae8615cf925e52b980b093749766c1..70d9062f0e5d69d7585289234f4de97f0625049c 100644 --- a/src/plugins/server/jbuffer.mli +++ b/src/plugins/server/jbuffer.mli @@ -46,8 +46,8 @@ val bprintf : buffer -> ('a,Format.formatter,unit) format -> 'a val append : buffer -> string -> int -> int -> unit val flush : buffer -> unit -> unit -val push_tag : buffer -> Format.tag -> unit -val pop_tag : buffer -> Format.tag -> unit +val push_tag : buffer -> Transitioning.Format.stag -> unit +val pop_tag : buffer -> Transitioning.Format.stag -> unit (** Flushes the buffer and returns its JSON enoding. This pops all pending tags. *) diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml index f3236d745fca1b5aac4a16914c04ac6d7dca57ac..6ef092a72eab7bf4f88b45a3d292350f531d3aa8 100644 --- a/src/plugins/wp/Cfloat.ml +++ b/src/plugins/wp/Cfloat.ml @@ -305,7 +305,7 @@ module Compute = WpContext.StaticGenerator (struct type t = model * c_float * op - let compare = Pervasives.compare + let compare = Transitioning.Stdlib.compare let pretty fmt (m, ft, op) = Format.fprintf fmt "%s_%a_%s" (model_name m) pp_suffix ft (op_name op) diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml index d71aa0bb8cc132e7a844d95f7d671948f6ac56e8..8309cbf2a3b3d574b276322be18eaaefddef21c3 100644 --- a/src/plugins/wp/Layout.ml +++ b/src/plugins/wp/Layout.ml @@ -52,7 +52,7 @@ struct | _ , Field _ -> 1 | Index(ta,n) , Index(tb,m) -> let cmp = Typ.compare ta tb in - if cmp <> 0 then cmp else Pervasives.compare n m + if cmp <> 0 then cmp else Transitioning.Stdlib.compare n m let equal a b = (compare a b = 0) @@ -175,7 +175,7 @@ struct Usage.pretty fmt usage let compare ((da,ta):t) ((db,tb):t) = - let cmp = Pervasives.compare da db in + let cmp = Transitioning.Stdlib.compare da db in if cmp <> 0 then cmp else Typ.compare ta tb let equal a b = (compare a b = 0) diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml index 4e90766687443e8f45be82f7727d4b4804ffe93b..7a91fcd6fd1f8f2d14b4996940b9598c4917e91c 100644 --- a/src/plugins/wp/MemRegion.ml +++ b/src/plugins/wp/MemRegion.ml @@ -234,7 +234,7 @@ struct Format.fprintf fmt "}@]" ; end - let compare = Pervasives.compare + let compare = Transitioning.Stdlib.compare (* Extract constant offset *) let offset k = @@ -300,7 +300,7 @@ module ARRAY = struct type t = int * int list - let compare = Pervasives.compare + let compare = Transitioning.Stdlib.compare let pretty fmt (s,ds) = Format.fprintf fmt "%d%a" s Layout.Matrix.pretty ds (* Coefficient from Matrix dimensions: c_i = \Pi_{i Region.noid let hash m = id m - let compare m m' = if m==m then 0 else Pervasives.compare (id m) (id m') + let compare m m' = + if m==m then 0 else Transitioning.Stdlib.compare (id m) (id m') let equal m m' = m==m' || (id m = id m') let tau_of_value = function diff --git a/src/plugins/wp/Region.ml b/src/plugins/wp/Region.ml index dc77afe871e5063a16ec80c7a15e096c539fd10b..ceea978dcacd51e82218e84c3bea1fff10688dd2 100644 --- a/src/plugins/wp/Region.ml +++ b/src/plugins/wp/Region.ml @@ -128,7 +128,7 @@ struct type t = region let id a = a.id let equal a b = (a.id = b.id) - let compare a b = Pervasives.compare a.id b.id + let compare a b = Transitioning.Stdlib.compare a.id b.id let pp_rid fmt id = Format.fprintf fmt "R%03d" id let pretty fmt r = pp_rid fmt r.id end